0 JBC
↳1 JBCToGraph (⇒, 190 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 AND
↳5 JBCTerminationSCC
↳6 SCCToIDPv1Proof (⇒, 20 ms)
↳7 IDP
↳8 IDPNonInfProof (⇒, 70 ms)
↳9 AND
↳10 IDP
↳11 IDependencyGraphProof (⇔, 0 ms)
↳12 TRUE
↳13 IDP
↳14 IDependencyGraphProof (⇔, 0 ms)
↳15 TRUE
↳16 JBCTerminationSCC
↳17 SCCToIDPv1Proof (⇒, 40 ms)
↳18 IDP
↳19 IDPNonInfProof (⇒, 80 ms)
↳20 AND
↳21 IDP
↳22 IDependencyGraphProof (⇔, 0 ms)
↳23 TRUE
↳24 IDP
↳25 IDependencyGraphProof (⇔, 0 ms)
↳26 TRUE
↳27 JBCTerminationSCC
↳28 SCCToIDPv1Proof (⇒, 50 ms)
↳29 IDP
↳30 IDPNonInfProof (⇒, 80 ms)
↳31 AND
↳32 IDP
↳33 IDependencyGraphProof (⇔, 0 ms)
↳34 TRUE
↳35 IDP
↳36 IDependencyGraphProof (⇔, 0 ms)
↳37 TRUE
↳38 JBCTerminationSCC
↳39 SCCToIDPv1Proof (⇒, 20 ms)
↳40 IDP
↳41 IDPNonInfProof (⇒, 70 ms)
↳42 AND
↳43 IDP
↳44 IDependencyGraphProof (⇔, 0 ms)
↳45 TRUE
↳46 IDP
↳47 IDependencyGraphProof (⇔, 0 ms)
↳48 TRUE
↳49 JBCTerminationSCC
↳50 SCCToIDPv1Proof (⇒, 40 ms)
↳51 IDP
↳52 IDPNonInfProof (⇒, 70 ms)
↳53 AND
↳54 IDP
↳55 IDependencyGraphProof (⇔, 0 ms)
↳56 TRUE
↳57 IDP
↳58 IDependencyGraphProof (⇔, 0 ms)
↳59 TRUE
↳60 JBCTerminationSCC
↳61 SCCToIDPv1Proof (⇒, 30 ms)
↳62 IDP
↳63 IDPNonInfProof (⇒, 50 ms)
↳64 AND
↳65 IDP
↳66 IDependencyGraphProof (⇔, 0 ms)
↳67 TRUE
↳68 IDP
↳69 IDependencyGraphProof (⇔, 0 ms)
↳70 TRUE
↳71 JBCTerminationSCC
↳72 SCCToIDPv1Proof (⇒, 30 ms)
↳73 IDP
↳74 IDPNonInfProof (⇒, 80 ms)
↳75 AND
↳76 IDP
↳77 IDependencyGraphProof (⇔, 0 ms)
↳78 TRUE
↳79 IDP
↳80 IDependencyGraphProof (⇔, 0 ms)
↳81 TRUE
↳82 JBCTerminationSCC
↳83 SCCToIDPv1Proof (⇒, 20 ms)
↳84 IDP
↳85 IDPNonInfProof (⇒, 70 ms)
↳86 AND
↳87 IDP
↳88 IDependencyGraphProof (⇔, 0 ms)
↳89 TRUE
↳90 IDP
↳91 IDependencyGraphProof (⇔, 0 ms)
↳92 TRUE
↳93 JBCTerminationSCC
↳94 SCCToIDPv1Proof (⇒, 40 ms)
↳95 IDP
↳96 IDPNonInfProof (⇒, 70 ms)
↳97 AND
↳98 IDP
↳99 IDependencyGraphProof (⇔, 0 ms)
↳100 TRUE
↳101 IDP
↳102 IDependencyGraphProof (⇔, 0 ms)
↳103 TRUE
↳104 JBCTerminationSCC
↳105 SCCToIDPv1Proof (⇒, 30 ms)
↳106 IDP
↳107 IDPNonInfProof (⇒, 60 ms)
↳108 AND
↳109 IDP
↳110 IDependencyGraphProof (⇔, 0 ms)
↳111 TRUE
↳112 IDP
↳113 IDependencyGraphProof (⇔, 0 ms)
↳114 TRUE
↳115 JBCTerminationSCC
↳116 SCCToIDPv1Proof (⇒, 30 ms)
↳117 IDP
↳118 IDPNonInfProof (⇒, 90 ms)
↳119 AND
↳120 IDP
↳121 IDependencyGraphProof (⇔, 0 ms)
↳122 TRUE
↳123 IDP
↳124 IDependencyGraphProof (⇔, 0 ms)
↳125 TRUE
↳126 JBCTerminationSCC
↳127 SCCToIDPv1Proof (⇒, 40 ms)
↳128 IDP
↳129 IDPNonInfProof (⇒, 70 ms)
↳130 AND
↳131 IDP
↳132 IDependencyGraphProof (⇔, 0 ms)
↳133 TRUE
↳134 IDP
↳135 IDependencyGraphProof (⇔, 0 ms)
↳136 TRUE
↳137 JBCTerminationSCC
↳138 SCCToIDPv1Proof (⇒, 770 ms)
↳139 IDP
↳140 IDPNonInfProof (⇒, 650 ms)
↳141 AND
↳142 IDP
↳143 IDependencyGraphProof (⇔, 0 ms)
↳144 IDP
↳145 IDPNonInfProof (⇒, 340 ms)
↳146 AND
↳147 IDP
↳148 IDependencyGraphProof (⇔, 0 ms)
↳149 TRUE
↳150 IDP
↳151 IDependencyGraphProof (⇔, 0 ms)
↳152 TRUE
↳153 IDP
↳154 IDependencyGraphProof (⇔, 0 ms)
↳155 IDP
↳156 IDPNonInfProof (⇒, 540 ms)
↳157 AND
↳158 IDP
↳159 IDependencyGraphProof (⇔, 0 ms)
↳160 TRUE
↳161 IDP
↳162 IDependencyGraphProof (⇔, 0 ms)
↳163 TRUE
public class Test9 {
public static void main(String[] args) {
long l = args.length;
while (l > 0) {
for (int i = (int) l ; i < 100; i++)
test(i);
l--;
}
}
private static void test(int i) {
int j, k, l, m;
for (j = i; j > 0; j--);
for (k = i; k > 0; k--);
for (l = i; l > 0; l--);
for (m = i; m > 0; m--);
for (j = i; j > 0; j--);
for (k = i; k > 0; k--);
for (l = i; l > 0; l--);
for (m = i; m > 0; m--);
for (j = i; j > 0; j--);
for (k = i; k > 0; k--);
for (l = i; l > 0; l--);
for (m = i; m > 0; m--);
}
}
Generated 6 rules for P and 0 rules for R.
P rules:
746_0_test_LE(EOS(STATIC_746), i208, i208) → 750_0_test_LE(EOS(STATIC_750), i208, i208)
750_0_test_LE(EOS(STATIC_750), i208, i208) → 753_0_test_Inc(EOS(STATIC_753), i208) | >(i208, 0)
753_0_test_Inc(EOS(STATIC_753), i208) → 759_0_test_JMP(EOS(STATIC_759), +(i208, -1)) | >(i208, 0)
759_0_test_JMP(EOS(STATIC_759), i211) → 770_0_test_Load(EOS(STATIC_770), i211)
770_0_test_Load(EOS(STATIC_770), i211) → 744_0_test_Load(EOS(STATIC_744), i211)
744_0_test_Load(EOS(STATIC_744), i203) → 746_0_test_LE(EOS(STATIC_746), i203, i203)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
746_0_test_LE(EOS(STATIC_746), x0, x0) → 746_0_test_LE(EOS(STATIC_746), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
746_0_test_LE(x1, x2, x3) → 746_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_746_0_test_LE(x1, x2, x3, x4) → Cond_746_0_test_LE(x1, x3, x4)
Filtered duplicate args:
746_0_test_LE(x1, x2) → 746_0_test_LE(x2)
Cond_746_0_test_LE(x1, x2, x3) → Cond_746_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
746_0_test_LE(x0) → 746_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
746_0_TEST_LE(x0) → COND_746_0_TEST_LE(>(x0, 0), x0)
COND_746_0_TEST_LE(TRUE, x0) → 746_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 746_0_TEST_LE(x0[0])≥NonInfC∧746_0_TEST_LE(x0[0])≥COND_746_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_746_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 746_0_TEST_LE(x0[0])≥NonInfC∧746_0_TEST_LE(x0[0])≥COND_746_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_746_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_746_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_746_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_746_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_746_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_746_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_746_0_TEST_LE(TRUE, x0[1])≥746_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(746_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(746_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(746_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(746_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(746_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(746_0_TEST_LE(x1)) = [2]x1
POL(COND_746_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_746_0_TEST_LE(TRUE, x0[1]) → 746_0_TEST_LE(+(x0[1], -1))
746_0_TEST_LE(x0[0]) → COND_746_0_TEST_LE(>(x0[0], 0), x0[0])
746_0_TEST_LE(x0[0]) → COND_746_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
715_0_test_LE(EOS(STATIC_715), i197, i197) → 718_0_test_LE(EOS(STATIC_718), i197, i197)
718_0_test_LE(EOS(STATIC_718), i197, i197) → 722_0_test_Inc(EOS(STATIC_722), i197) | >(i197, 0)
722_0_test_Inc(EOS(STATIC_722), i197) → 726_0_test_JMP(EOS(STATIC_726), +(i197, -1)) | >(i197, 0)
726_0_test_JMP(EOS(STATIC_726), i199) → 731_0_test_Load(EOS(STATIC_731), i199)
731_0_test_Load(EOS(STATIC_731), i199) → 713_0_test_Load(EOS(STATIC_713), i199)
713_0_test_Load(EOS(STATIC_713), i194) → 715_0_test_LE(EOS(STATIC_715), i194, i194)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
715_0_test_LE(EOS(STATIC_715), x0, x0) → 715_0_test_LE(EOS(STATIC_715), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
715_0_test_LE(x1, x2, x3) → 715_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_715_0_test_LE(x1, x2, x3, x4) → Cond_715_0_test_LE(x1, x3, x4)
Filtered duplicate args:
715_0_test_LE(x1, x2) → 715_0_test_LE(x2)
Cond_715_0_test_LE(x1, x2, x3) → Cond_715_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
715_0_test_LE(x0) → 715_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
715_0_TEST_LE(x0) → COND_715_0_TEST_LE(>(x0, 0), x0)
COND_715_0_TEST_LE(TRUE, x0) → 715_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 715_0_TEST_LE(x0[0])≥NonInfC∧715_0_TEST_LE(x0[0])≥COND_715_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_715_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 715_0_TEST_LE(x0[0])≥NonInfC∧715_0_TEST_LE(x0[0])≥COND_715_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_715_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_715_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_715_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_715_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_715_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_715_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_715_0_TEST_LE(TRUE, x0[1])≥715_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(715_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(715_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(715_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(715_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(715_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(715_0_TEST_LE(x1)) = [2]x1
POL(COND_715_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_715_0_TEST_LE(TRUE, x0[1]) → 715_0_TEST_LE(+(x0[1], -1))
715_0_TEST_LE(x0[0]) → COND_715_0_TEST_LE(>(x0[0], 0), x0[0])
715_0_TEST_LE(x0[0]) → COND_715_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
680_0_test_LE(EOS(STATIC_680), i189, i189) → 683_0_test_LE(EOS(STATIC_683), i189, i189)
683_0_test_LE(EOS(STATIC_683), i189, i189) → 688_0_test_Inc(EOS(STATIC_688), i189) | >(i189, 0)
688_0_test_Inc(EOS(STATIC_688), i189) → 692_0_test_JMP(EOS(STATIC_692), +(i189, -1)) | >(i189, 0)
692_0_test_JMP(EOS(STATIC_692), i191) → 699_0_test_Load(EOS(STATIC_699), i191)
699_0_test_Load(EOS(STATIC_699), i191) → 676_0_test_Load(EOS(STATIC_676), i191)
676_0_test_Load(EOS(STATIC_676), i184) → 680_0_test_LE(EOS(STATIC_680), i184, i184)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
680_0_test_LE(EOS(STATIC_680), x0, x0) → 680_0_test_LE(EOS(STATIC_680), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
680_0_test_LE(x1, x2, x3) → 680_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_680_0_test_LE(x1, x2, x3, x4) → Cond_680_0_test_LE(x1, x3, x4)
Filtered duplicate args:
680_0_test_LE(x1, x2) → 680_0_test_LE(x2)
Cond_680_0_test_LE(x1, x2, x3) → Cond_680_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
680_0_test_LE(x0) → 680_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
680_0_TEST_LE(x0) → COND_680_0_TEST_LE(>(x0, 0), x0)
COND_680_0_TEST_LE(TRUE, x0) → 680_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 680_0_TEST_LE(x0[0])≥NonInfC∧680_0_TEST_LE(x0[0])≥COND_680_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_680_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 680_0_TEST_LE(x0[0])≥NonInfC∧680_0_TEST_LE(x0[0])≥COND_680_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_680_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_680_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_680_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_680_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_680_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_680_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_680_0_TEST_LE(TRUE, x0[1])≥680_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(680_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(680_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(680_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(680_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(680_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(680_0_TEST_LE(x1)) = [2]x1
POL(COND_680_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_680_0_TEST_LE(TRUE, x0[1]) → 680_0_TEST_LE(+(x0[1], -1))
680_0_TEST_LE(x0[0]) → COND_680_0_TEST_LE(>(x0[0], 0), x0[0])
680_0_TEST_LE(x0[0]) → COND_680_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
641_0_test_LE(EOS(STATIC_641), i173, i173) → 645_0_test_LE(EOS(STATIC_645), i173, i173)
645_0_test_LE(EOS(STATIC_645), i173, i173) → 649_0_test_Inc(EOS(STATIC_649), i173) | >(i173, 0)
649_0_test_Inc(EOS(STATIC_649), i173) → 654_0_test_JMP(EOS(STATIC_654), +(i173, -1)) | >(i173, 0)
654_0_test_JMP(EOS(STATIC_654), i177) → 660_0_test_Load(EOS(STATIC_660), i177)
660_0_test_Load(EOS(STATIC_660), i177) → 637_0_test_Load(EOS(STATIC_637), i177)
637_0_test_Load(EOS(STATIC_637), i169) → 641_0_test_LE(EOS(STATIC_641), i169, i169)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
641_0_test_LE(EOS(STATIC_641), x0, x0) → 641_0_test_LE(EOS(STATIC_641), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
641_0_test_LE(x1, x2, x3) → 641_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_641_0_test_LE(x1, x2, x3, x4) → Cond_641_0_test_LE(x1, x3, x4)
Filtered duplicate args:
641_0_test_LE(x1, x2) → 641_0_test_LE(x2)
Cond_641_0_test_LE(x1, x2, x3) → Cond_641_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
641_0_test_LE(x0) → 641_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
641_0_TEST_LE(x0) → COND_641_0_TEST_LE(>(x0, 0), x0)
COND_641_0_TEST_LE(TRUE, x0) → 641_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 641_0_TEST_LE(x0[0])≥NonInfC∧641_0_TEST_LE(x0[0])≥COND_641_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_641_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 641_0_TEST_LE(x0[0])≥NonInfC∧641_0_TEST_LE(x0[0])≥COND_641_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_641_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_641_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_641_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_641_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_641_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_641_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_641_0_TEST_LE(TRUE, x0[1])≥641_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(641_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(641_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(641_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(641_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(641_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(641_0_TEST_LE(x1)) = [2]x1
POL(COND_641_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_641_0_TEST_LE(TRUE, x0[1]) → 641_0_TEST_LE(+(x0[1], -1))
641_0_TEST_LE(x0[0]) → COND_641_0_TEST_LE(>(x0[0], 0), x0[0])
641_0_TEST_LE(x0[0]) → COND_641_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
602_0_test_LE(EOS(STATIC_602), i161, i161) → 606_0_test_LE(EOS(STATIC_606), i161, i161)
606_0_test_LE(EOS(STATIC_606), i161, i161) → 610_0_test_Inc(EOS(STATIC_610), i161) | >(i161, 0)
610_0_test_Inc(EOS(STATIC_610), i161) → 614_0_test_JMP(EOS(STATIC_614), +(i161, -1)) | >(i161, 0)
614_0_test_JMP(EOS(STATIC_614), i163) → 621_0_test_Load(EOS(STATIC_621), i163)
621_0_test_Load(EOS(STATIC_621), i163) → 598_0_test_Load(EOS(STATIC_598), i163)
598_0_test_Load(EOS(STATIC_598), i157) → 602_0_test_LE(EOS(STATIC_602), i157, i157)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
602_0_test_LE(EOS(STATIC_602), x0, x0) → 602_0_test_LE(EOS(STATIC_602), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
602_0_test_LE(x1, x2, x3) → 602_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_602_0_test_LE(x1, x2, x3, x4) → Cond_602_0_test_LE(x1, x3, x4)
Filtered duplicate args:
602_0_test_LE(x1, x2) → 602_0_test_LE(x2)
Cond_602_0_test_LE(x1, x2, x3) → Cond_602_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
602_0_test_LE(x0) → 602_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
602_0_TEST_LE(x0) → COND_602_0_TEST_LE(>(x0, 0), x0)
COND_602_0_TEST_LE(TRUE, x0) → 602_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 602_0_TEST_LE(x0[0])≥NonInfC∧602_0_TEST_LE(x0[0])≥COND_602_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_602_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 602_0_TEST_LE(x0[0])≥NonInfC∧602_0_TEST_LE(x0[0])≥COND_602_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_602_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_602_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_602_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_602_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_602_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_602_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_602_0_TEST_LE(TRUE, x0[1])≥602_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(602_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(602_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(602_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(602_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(602_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(602_0_TEST_LE(x1)) = [2]x1
POL(COND_602_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_602_0_TEST_LE(TRUE, x0[1]) → 602_0_TEST_LE(+(x0[1], -1))
602_0_TEST_LE(x0[0]) → COND_602_0_TEST_LE(>(x0[0], 0), x0[0])
602_0_TEST_LE(x0[0]) → COND_602_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
564_0_test_LE(EOS(STATIC_564), i148, i148) → 568_0_test_LE(EOS(STATIC_568), i148, i148)
568_0_test_LE(EOS(STATIC_568), i148, i148) → 572_0_test_Inc(EOS(STATIC_572), i148) | >(i148, 0)
572_0_test_Inc(EOS(STATIC_572), i148) → 577_0_test_JMP(EOS(STATIC_577), +(i148, -1)) | >(i148, 0)
577_0_test_JMP(EOS(STATIC_577), i151) → 583_0_test_Load(EOS(STATIC_583), i151)
583_0_test_Load(EOS(STATIC_583), i151) → 561_0_test_Load(EOS(STATIC_561), i151)
561_0_test_Load(EOS(STATIC_561), i143) → 564_0_test_LE(EOS(STATIC_564), i143, i143)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
564_0_test_LE(EOS(STATIC_564), x0, x0) → 564_0_test_LE(EOS(STATIC_564), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
564_0_test_LE(x1, x2, x3) → 564_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_564_0_test_LE(x1, x2, x3, x4) → Cond_564_0_test_LE(x1, x3, x4)
Filtered duplicate args:
564_0_test_LE(x1, x2) → 564_0_test_LE(x2)
Cond_564_0_test_LE(x1, x2, x3) → Cond_564_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
564_0_test_LE(x0) → 564_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
564_0_TEST_LE(x0) → COND_564_0_TEST_LE(>(x0, 0), x0)
COND_564_0_TEST_LE(TRUE, x0) → 564_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 564_0_TEST_LE(x0[0])≥NonInfC∧564_0_TEST_LE(x0[0])≥COND_564_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_564_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 564_0_TEST_LE(x0[0])≥NonInfC∧564_0_TEST_LE(x0[0])≥COND_564_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_564_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_564_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_564_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_564_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_564_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_564_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_564_0_TEST_LE(TRUE, x0[1])≥564_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(564_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(564_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(564_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(564_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(564_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(564_0_TEST_LE(x1)) = [2]x1
POL(COND_564_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_564_0_TEST_LE(TRUE, x0[1]) → 564_0_TEST_LE(+(x0[1], -1))
564_0_TEST_LE(x0[0]) → COND_564_0_TEST_LE(>(x0[0], 0), x0[0])
564_0_TEST_LE(x0[0]) → COND_564_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
528_0_test_LE(EOS(STATIC_528), i136, i136) → 531_0_test_LE(EOS(STATIC_531), i136, i136)
531_0_test_LE(EOS(STATIC_531), i136, i136) → 535_0_test_Inc(EOS(STATIC_535), i136) | >(i136, 0)
535_0_test_Inc(EOS(STATIC_535), i136) → 539_0_test_JMP(EOS(STATIC_539), +(i136, -1)) | >(i136, 0)
539_0_test_JMP(EOS(STATIC_539), i138) → 545_0_test_Load(EOS(STATIC_545), i138)
545_0_test_Load(EOS(STATIC_545), i138) → 525_0_test_Load(EOS(STATIC_525), i138)
525_0_test_Load(EOS(STATIC_525), i131) → 528_0_test_LE(EOS(STATIC_528), i131, i131)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
528_0_test_LE(EOS(STATIC_528), x0, x0) → 528_0_test_LE(EOS(STATIC_528), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
528_0_test_LE(x1, x2, x3) → 528_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_528_0_test_LE(x1, x2, x3, x4) → Cond_528_0_test_LE(x1, x3, x4)
Filtered duplicate args:
528_0_test_LE(x1, x2) → 528_0_test_LE(x2)
Cond_528_0_test_LE(x1, x2, x3) → Cond_528_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
528_0_test_LE(x0) → 528_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
528_0_TEST_LE(x0) → COND_528_0_TEST_LE(>(x0, 0), x0)
COND_528_0_TEST_LE(TRUE, x0) → 528_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 528_0_TEST_LE(x0[0])≥NonInfC∧528_0_TEST_LE(x0[0])≥COND_528_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_528_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 528_0_TEST_LE(x0[0])≥NonInfC∧528_0_TEST_LE(x0[0])≥COND_528_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_528_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_528_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_528_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_528_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_528_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_528_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_528_0_TEST_LE(TRUE, x0[1])≥528_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(528_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(528_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(528_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(528_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(528_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(528_0_TEST_LE(x1)) = [2]x1
POL(COND_528_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_528_0_TEST_LE(TRUE, x0[1]) → 528_0_TEST_LE(+(x0[1], -1))
528_0_TEST_LE(x0[0]) → COND_528_0_TEST_LE(>(x0[0], 0), x0[0])
528_0_TEST_LE(x0[0]) → COND_528_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
496_0_test_LE(EOS(STATIC_496), i125, i125) → 500_0_test_LE(EOS(STATIC_500), i125, i125)
500_0_test_LE(EOS(STATIC_500), i125, i125) → 504_0_test_Inc(EOS(STATIC_504), i125) | >(i125, 0)
504_0_test_Inc(EOS(STATIC_504), i125) → 509_0_test_JMP(EOS(STATIC_509), +(i125, -1)) | >(i125, 0)
509_0_test_JMP(EOS(STATIC_509), i127) → 514_0_test_Load(EOS(STATIC_514), i127)
514_0_test_Load(EOS(STATIC_514), i127) → 493_0_test_Load(EOS(STATIC_493), i127)
493_0_test_Load(EOS(STATIC_493), i121) → 496_0_test_LE(EOS(STATIC_496), i121, i121)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
496_0_test_LE(EOS(STATIC_496), x0, x0) → 496_0_test_LE(EOS(STATIC_496), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
496_0_test_LE(x1, x2, x3) → 496_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_496_0_test_LE(x1, x2, x3, x4) → Cond_496_0_test_LE(x1, x3, x4)
Filtered duplicate args:
496_0_test_LE(x1, x2) → 496_0_test_LE(x2)
Cond_496_0_test_LE(x1, x2, x3) → Cond_496_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
496_0_test_LE(x0) → 496_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
496_0_TEST_LE(x0) → COND_496_0_TEST_LE(>(x0, 0), x0)
COND_496_0_TEST_LE(TRUE, x0) → 496_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 496_0_TEST_LE(x0[0])≥NonInfC∧496_0_TEST_LE(x0[0])≥COND_496_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_496_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 496_0_TEST_LE(x0[0])≥NonInfC∧496_0_TEST_LE(x0[0])≥COND_496_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_496_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_496_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_496_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_496_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_496_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_496_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_496_0_TEST_LE(TRUE, x0[1])≥496_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(496_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(496_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(496_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(496_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(496_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(496_0_TEST_LE(x1)) = [2]x1
POL(COND_496_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_496_0_TEST_LE(TRUE, x0[1]) → 496_0_TEST_LE(+(x0[1], -1))
496_0_TEST_LE(x0[0]) → COND_496_0_TEST_LE(>(x0[0], 0), x0[0])
496_0_TEST_LE(x0[0]) → COND_496_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
456_0_test_LE(EOS(STATIC_456), i115, i115) → 460_0_test_LE(EOS(STATIC_460), i115, i115)
460_0_test_LE(EOS(STATIC_460), i115, i115) → 464_0_test_Inc(EOS(STATIC_464), i115) | >(i115, 0)
464_0_test_Inc(EOS(STATIC_464), i115) → 470_0_test_JMP(EOS(STATIC_470), +(i115, -1)) | >(i115, 0)
470_0_test_JMP(EOS(STATIC_470), i118) → 476_0_test_Load(EOS(STATIC_476), i118)
476_0_test_Load(EOS(STATIC_476), i118) → 452_0_test_Load(EOS(STATIC_452), i118)
452_0_test_Load(EOS(STATIC_452), i108) → 456_0_test_LE(EOS(STATIC_456), i108, i108)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
456_0_test_LE(EOS(STATIC_456), x0, x0) → 456_0_test_LE(EOS(STATIC_456), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
456_0_test_LE(x1, x2, x3) → 456_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_456_0_test_LE(x1, x2, x3, x4) → Cond_456_0_test_LE(x1, x3, x4)
Filtered duplicate args:
456_0_test_LE(x1, x2) → 456_0_test_LE(x2)
Cond_456_0_test_LE(x1, x2, x3) → Cond_456_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
456_0_test_LE(x0) → 456_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
456_0_TEST_LE(x0) → COND_456_0_TEST_LE(>(x0, 0), x0)
COND_456_0_TEST_LE(TRUE, x0) → 456_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 456_0_TEST_LE(x0[0])≥NonInfC∧456_0_TEST_LE(x0[0])≥COND_456_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_456_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 456_0_TEST_LE(x0[0])≥NonInfC∧456_0_TEST_LE(x0[0])≥COND_456_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_456_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_456_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_456_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_456_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_456_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_456_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_456_0_TEST_LE(TRUE, x0[1])≥456_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(456_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(456_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(456_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(456_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(456_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(456_0_TEST_LE(x1)) = [2]x1
POL(COND_456_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_456_0_TEST_LE(TRUE, x0[1]) → 456_0_TEST_LE(+(x0[1], -1))
456_0_TEST_LE(x0[0]) → COND_456_0_TEST_LE(>(x0[0], 0), x0[0])
456_0_TEST_LE(x0[0]) → COND_456_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
416_0_test_LE(EOS(STATIC_416), i102, i102) → 419_0_test_LE(EOS(STATIC_419), i102, i102)
419_0_test_LE(EOS(STATIC_419), i102, i102) → 423_0_test_Inc(EOS(STATIC_423), i102) | >(i102, 0)
423_0_test_Inc(EOS(STATIC_423), i102) → 428_0_test_JMP(EOS(STATIC_428), +(i102, -1)) | >(i102, 0)
428_0_test_JMP(EOS(STATIC_428), i103) → 435_0_test_Load(EOS(STATIC_435), i103)
435_0_test_Load(EOS(STATIC_435), i103) → 413_0_test_Load(EOS(STATIC_413), i103)
413_0_test_Load(EOS(STATIC_413), i98) → 416_0_test_LE(EOS(STATIC_416), i98, i98)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
416_0_test_LE(EOS(STATIC_416), x0, x0) → 416_0_test_LE(EOS(STATIC_416), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
416_0_test_LE(x1, x2, x3) → 416_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_416_0_test_LE(x1, x2, x3, x4) → Cond_416_0_test_LE(x1, x3, x4)
Filtered duplicate args:
416_0_test_LE(x1, x2) → 416_0_test_LE(x2)
Cond_416_0_test_LE(x1, x2, x3) → Cond_416_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
416_0_test_LE(x0) → 416_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
416_0_TEST_LE(x0) → COND_416_0_TEST_LE(>(x0, 0), x0)
COND_416_0_TEST_LE(TRUE, x0) → 416_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 416_0_TEST_LE(x0[0])≥NonInfC∧416_0_TEST_LE(x0[0])≥COND_416_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_416_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 416_0_TEST_LE(x0[0])≥NonInfC∧416_0_TEST_LE(x0[0])≥COND_416_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_416_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_416_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_416_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_416_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_416_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_416_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_416_0_TEST_LE(TRUE, x0[1])≥416_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(416_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(416_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(416_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(416_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(416_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(416_0_TEST_LE(x1)) = [2]x1
POL(COND_416_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_416_0_TEST_LE(TRUE, x0[1]) → 416_0_TEST_LE(+(x0[1], -1))
416_0_TEST_LE(x0[0]) → COND_416_0_TEST_LE(>(x0[0], 0), x0[0])
416_0_TEST_LE(x0[0]) → COND_416_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
389_0_test_LE(EOS(STATIC_389), i91, i91) → 392_0_test_LE(EOS(STATIC_392), i91, i91)
392_0_test_LE(EOS(STATIC_392), i91, i91) → 396_0_test_Inc(EOS(STATIC_396), i91) | >(i91, 0)
396_0_test_Inc(EOS(STATIC_396), i91) → 400_0_test_JMP(EOS(STATIC_400), +(i91, -1)) | >(i91, 0)
400_0_test_JMP(EOS(STATIC_400), i94) → 405_0_test_Load(EOS(STATIC_405), i94)
405_0_test_Load(EOS(STATIC_405), i94) → 386_0_test_Load(EOS(STATIC_386), i94)
386_0_test_Load(EOS(STATIC_386), i86) → 389_0_test_LE(EOS(STATIC_389), i86, i86)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
389_0_test_LE(EOS(STATIC_389), x0, x0) → 389_0_test_LE(EOS(STATIC_389), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
389_0_test_LE(x1, x2, x3) → 389_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_389_0_test_LE(x1, x2, x3, x4) → Cond_389_0_test_LE(x1, x3, x4)
Filtered duplicate args:
389_0_test_LE(x1, x2) → 389_0_test_LE(x2)
Cond_389_0_test_LE(x1, x2, x3) → Cond_389_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
389_0_test_LE(x0) → 389_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
389_0_TEST_LE(x0) → COND_389_0_TEST_LE(>(x0, 0), x0)
COND_389_0_TEST_LE(TRUE, x0) → 389_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 389_0_TEST_LE(x0[0])≥NonInfC∧389_0_TEST_LE(x0[0])≥COND_389_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_389_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 389_0_TEST_LE(x0[0])≥NonInfC∧389_0_TEST_LE(x0[0])≥COND_389_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_389_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_389_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_389_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_389_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_389_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_389_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_389_0_TEST_LE(TRUE, x0[1])≥389_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(389_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(389_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(389_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(389_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(389_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(389_0_TEST_LE(x1)) = [2]x1
POL(COND_389_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_389_0_TEST_LE(TRUE, x0[1]) → 389_0_TEST_LE(+(x0[1], -1))
389_0_TEST_LE(x0[0]) → COND_389_0_TEST_LE(>(x0[0], 0), x0[0])
389_0_TEST_LE(x0[0]) → COND_389_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
356_0_test_LE(EOS(STATIC_356), i79, i79) → 360_0_test_LE(EOS(STATIC_360), i79, i79)
360_0_test_LE(EOS(STATIC_360), i79, i79) → 364_0_test_Inc(EOS(STATIC_364), i79) | >(i79, 0)
364_0_test_Inc(EOS(STATIC_364), i79) → 368_0_test_JMP(EOS(STATIC_368), +(i79, -1)) | >(i79, 0)
368_0_test_JMP(EOS(STATIC_368), i81) → 373_0_test_Load(EOS(STATIC_373), i81)
373_0_test_Load(EOS(STATIC_373), i81) → 352_0_test_Load(EOS(STATIC_352), i81)
352_0_test_Load(EOS(STATIC_352), i73) → 356_0_test_LE(EOS(STATIC_356), i73, i73)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
356_0_test_LE(EOS(STATIC_356), x0, x0) → 356_0_test_LE(EOS(STATIC_356), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
356_0_test_LE(x1, x2, x3) → 356_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_356_0_test_LE(x1, x2, x3, x4) → Cond_356_0_test_LE(x1, x3, x4)
Filtered duplicate args:
356_0_test_LE(x1, x2) → 356_0_test_LE(x2)
Cond_356_0_test_LE(x1, x2, x3) → Cond_356_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
356_0_test_LE(x0) → 356_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
356_0_TEST_LE(x0) → COND_356_0_TEST_LE(>(x0, 0), x0)
COND_356_0_TEST_LE(TRUE, x0) → 356_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 356_0_TEST_LE(x0[0])≥NonInfC∧356_0_TEST_LE(x0[0])≥COND_356_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_356_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 356_0_TEST_LE(x0[0])≥NonInfC∧356_0_TEST_LE(x0[0])≥COND_356_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_356_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_356_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_356_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_356_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_356_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_356_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_356_0_TEST_LE(TRUE, x0[1])≥356_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(356_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(356_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(356_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(356_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(356_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(356_0_TEST_LE(x1)) = [2]x1
POL(COND_356_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_356_0_TEST_LE(TRUE, x0[1]) → 356_0_TEST_LE(+(x0[1], -1))
356_0_TEST_LE(x0[0]) → COND_356_0_TEST_LE(>(x0[0], 0), x0[0])
356_0_TEST_LE(x0[0]) → COND_356_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 27 rules for P and 134 rules for R.
P rules:
62_0_main_ConstantStackPush(EOS(STATIC_62), i4, i4) → 64_0_main_Cmp(EOS(STATIC_64), i4, i4, 0)
64_0_main_Cmp(EOS(STATIC_64), i6, i6, matching1) → 68_0_main_Cmp(EOS(STATIC_68), i6, i6, 0) | =(matching1, 0)
68_0_main_Cmp(EOS(STATIC_68), i6, i6, matching1) → 76_0_main_LE(EOS(STATIC_76), i6, 1) | &&(>(i6, 0), =(matching1, 0))
76_0_main_LE(EOS(STATIC_76), i6, matching1) → 80_0_main_Load(EOS(STATIC_80), i6) | &&(>(1, 0), =(matching1, 1))
80_0_main_Load(EOS(STATIC_80), i6) → 84_0_main_TypeCast(EOS(STATIC_84), i6, i6)
84_0_main_TypeCast(EOS(STATIC_84), i6, i6) → 86_0_main_Store(EOS(STATIC_86), i6, i10) | =(i10, i6)
86_0_main_Store(EOS(STATIC_86), i6, i10) → 88_0_main_Load(EOS(STATIC_88), i6, i10)
88_0_main_Load(EOS(STATIC_88), i6, i10) → 89_0_main_ConstantStackPush(EOS(STATIC_89), i6, i10, i10)
89_0_main_ConstantStackPush(EOS(STATIC_89), i6, i10, i10) → 90_0_main_GE(EOS(STATIC_90), i6, i10, i10, 100)
90_0_main_GE(EOS(STATIC_90), i6, i13, i13, matching1) → 91_0_main_GE(EOS(STATIC_91), i6, i13, i13, 100) | =(matching1, 100)
90_0_main_GE(EOS(STATIC_90), i6, i14, i14, matching1) → 92_0_main_GE(EOS(STATIC_92), i6, i14, i14, 100) | =(matching1, 100)
91_0_main_GE(EOS(STATIC_91), i6, i13, i13, matching1) → 93_0_main_Load(EOS(STATIC_93), i6, i13) | &&(<(i13, 100), =(matching1, 100))
93_0_main_Load(EOS(STATIC_93), i6, i13) → 95_0_main_InvokeMethod(EOS(STATIC_95), i6, i13, i13)
95_0_main_InvokeMethod(EOS(STATIC_95), i6, i13, i13) → 97_1_main_InvokeMethod(97_0_test_Load(EOS(STATIC_97), i13), i6, i13, i13)
97_1_main_InvokeMethod(751_0_test_Return(EOS(STATIC_751)), i6, i215, i215) → 771_0_test_Return(EOS(STATIC_771), i6, i215, i215)
771_0_test_Return(EOS(STATIC_771), i6, i215, i215) → 774_0_main_Inc(EOS(STATIC_774), i6, i215)
774_0_main_Inc(EOS(STATIC_774), i6, i215) → 776_0_main_JMP(EOS(STATIC_776), i6, +(i215, 1)) | >(i215, 0)
776_0_main_JMP(EOS(STATIC_776), i6, i221) → 780_0_main_Load(EOS(STATIC_780), i6, i221)
780_0_main_Load(EOS(STATIC_780), i6, i221) → 88_0_main_Load(EOS(STATIC_88), i6, i221)
92_0_main_GE(EOS(STATIC_92), i6, i14, i14, matching1) → 94_0_main_Load(EOS(STATIC_94), i6) | &&(>=(i14, 100), =(matching1, 100))
94_0_main_Load(EOS(STATIC_94), i6) → 96_0_main_ConstantStackPush(EOS(STATIC_96), i6)
96_0_main_ConstantStackPush(EOS(STATIC_96), i6) → 100_0_main_IntArithmetic(EOS(STATIC_100), i6, 1)
100_0_main_IntArithmetic(EOS(STATIC_100), i6, matching1) → 104_0_main_Store(EOS(STATIC_104), -(i6, 1)) | &&(>(i6, 0), =(matching1, 1))
104_0_main_Store(EOS(STATIC_104), i16) → 108_0_main_JMP(EOS(STATIC_108), i16)
108_0_main_JMP(EOS(STATIC_108), i16) → 128_0_main_Load(EOS(STATIC_128), i16)
128_0_main_Load(EOS(STATIC_128), i16) → 60_0_main_Load(EOS(STATIC_60), i16)
60_0_main_Load(EOS(STATIC_60), i4) → 62_0_main_ConstantStackPush(EOS(STATIC_62), i4, i4)
R rules:
97_0_test_Load(EOS(STATIC_97), i13) → 102_0_test_Load(EOS(STATIC_102), i13)
102_0_test_Load(EOS(STATIC_102), i13) → 110_0_test_Load(EOS(STATIC_110), i13)
110_0_test_Load(EOS(STATIC_110), i13) → 131_0_test_Store(EOS(STATIC_131), i13, i13)
131_0_test_Store(EOS(STATIC_131), i13, i13) → 335_0_test_Load(EOS(STATIC_335), i13, i13)
335_0_test_Load(EOS(STATIC_335), i13, i13) → 352_0_test_Load(EOS(STATIC_352), i13, i13)
352_0_test_Load(EOS(STATIC_352), i13, i73) → 356_0_test_LE(EOS(STATIC_356), i13, i73, i73)
356_0_test_LE(EOS(STATIC_356), i13, matching1, matching2) → 359_0_test_LE(EOS(STATIC_359), i13, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
356_0_test_LE(EOS(STATIC_356), i13, i79, i79) → 360_0_test_LE(EOS(STATIC_360), i13, i79, i79)
359_0_test_LE(EOS(STATIC_359), i13, matching1, matching2) → 361_0_test_Load(EOS(STATIC_361), i13) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
360_0_test_LE(EOS(STATIC_360), i13, i79, i79) → 364_0_test_Inc(EOS(STATIC_364), i13, i79) | >(i79, 0)
361_0_test_Load(EOS(STATIC_361), i13) → 366_0_test_Store(EOS(STATIC_366), i13, i13)
364_0_test_Inc(EOS(STATIC_364), i13, i79) → 368_0_test_JMP(EOS(STATIC_368), i13, +(i79, -1)) | >(i79, 0)
366_0_test_Store(EOS(STATIC_366), i13, i13) → 370_0_test_Load(EOS(STATIC_370), i13, i13)
368_0_test_JMP(EOS(STATIC_368), i13, i81) → 373_0_test_Load(EOS(STATIC_373), i13, i81)
370_0_test_Load(EOS(STATIC_370), i13, i13) → 386_0_test_Load(EOS(STATIC_386), i13, i13)
373_0_test_Load(EOS(STATIC_373), i13, i81) → 352_0_test_Load(EOS(STATIC_352), i13, i81)
386_0_test_Load(EOS(STATIC_386), i13, i86) → 389_0_test_LE(EOS(STATIC_389), i13, i86, i86)
389_0_test_LE(EOS(STATIC_389), i13, matching1, matching2) → 391_0_test_LE(EOS(STATIC_391), i13, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
389_0_test_LE(EOS(STATIC_389), i13, i91, i91) → 392_0_test_LE(EOS(STATIC_392), i13, i91, i91)
391_0_test_LE(EOS(STATIC_391), i13, matching1, matching2) → 394_0_test_Load(EOS(STATIC_394), i13) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
392_0_test_LE(EOS(STATIC_392), i13, i91, i91) → 396_0_test_Inc(EOS(STATIC_396), i13, i91) | >(i91, 0)
394_0_test_Load(EOS(STATIC_394), i13) → 398_0_test_Store(EOS(STATIC_398), i13, i13)
396_0_test_Inc(EOS(STATIC_396), i13, i91) → 400_0_test_JMP(EOS(STATIC_400), i13, +(i91, -1)) | >(i91, 0)
398_0_test_Store(EOS(STATIC_398), i13, i13) → 401_0_test_Load(EOS(STATIC_401), i13, i13)
400_0_test_JMP(EOS(STATIC_400), i13, i94) → 405_0_test_Load(EOS(STATIC_405), i13, i94)
401_0_test_Load(EOS(STATIC_401), i13, i13) → 413_0_test_Load(EOS(STATIC_413), i13, i13)
405_0_test_Load(EOS(STATIC_405), i13, i94) → 386_0_test_Load(EOS(STATIC_386), i13, i94)
413_0_test_Load(EOS(STATIC_413), i13, i98) → 416_0_test_LE(EOS(STATIC_416), i13, i98, i98)
416_0_test_LE(EOS(STATIC_416), i13, matching1, matching2) → 418_0_test_LE(EOS(STATIC_418), i13, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
416_0_test_LE(EOS(STATIC_416), i13, i102, i102) → 419_0_test_LE(EOS(STATIC_419), i13, i102, i102)
418_0_test_LE(EOS(STATIC_418), i13, matching1, matching2) → 421_0_test_Load(EOS(STATIC_421), i13) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
419_0_test_LE(EOS(STATIC_419), i13, i102, i102) → 423_0_test_Inc(EOS(STATIC_423), i13, i102) | >(i102, 0)
421_0_test_Load(EOS(STATIC_421), i13) → 426_0_test_Store(EOS(STATIC_426), i13, i13)
423_0_test_Inc(EOS(STATIC_423), i13, i102) → 428_0_test_JMP(EOS(STATIC_428), i13, +(i102, -1)) | >(i102, 0)
426_0_test_Store(EOS(STATIC_426), i13, i13) → 431_0_test_Load(EOS(STATIC_431), i13, i13)
428_0_test_JMP(EOS(STATIC_428), i13, i103) → 435_0_test_Load(EOS(STATIC_435), i13, i103)
431_0_test_Load(EOS(STATIC_431), i13, i13) → 452_0_test_Load(EOS(STATIC_452), i13, i13)
435_0_test_Load(EOS(STATIC_435), i13, i103) → 413_0_test_Load(EOS(STATIC_413), i13, i103)
452_0_test_Load(EOS(STATIC_452), i13, i108) → 456_0_test_LE(EOS(STATIC_456), i13, i108, i108)
456_0_test_LE(EOS(STATIC_456), i13, matching1, matching2) → 459_0_test_LE(EOS(STATIC_459), i13, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
456_0_test_LE(EOS(STATIC_456), i13, i115, i115) → 460_0_test_LE(EOS(STATIC_460), i13, i115, i115)
459_0_test_LE(EOS(STATIC_459), i13, matching1, matching2) → 462_0_test_Load(EOS(STATIC_462), i13) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
460_0_test_LE(EOS(STATIC_460), i13, i115, i115) → 464_0_test_Inc(EOS(STATIC_464), i13, i115) | >(i115, 0)
462_0_test_Load(EOS(STATIC_462), i13) → 466_0_test_Store(EOS(STATIC_466), i13, i13)
464_0_test_Inc(EOS(STATIC_464), i13, i115) → 470_0_test_JMP(EOS(STATIC_470), i13, +(i115, -1)) | >(i115, 0)
466_0_test_Store(EOS(STATIC_466), i13, i13) → 472_0_test_Load(EOS(STATIC_472), i13, i13)
470_0_test_JMP(EOS(STATIC_470), i13, i118) → 476_0_test_Load(EOS(STATIC_476), i13, i118)
472_0_test_Load(EOS(STATIC_472), i13, i13) → 493_0_test_Load(EOS(STATIC_493), i13, i13)
476_0_test_Load(EOS(STATIC_476), i13, i118) → 452_0_test_Load(EOS(STATIC_452), i13, i118)
493_0_test_Load(EOS(STATIC_493), i13, i121) → 496_0_test_LE(EOS(STATIC_496), i13, i121, i121)
496_0_test_LE(EOS(STATIC_496), i13, matching1, matching2) → 499_0_test_LE(EOS(STATIC_499), i13, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
496_0_test_LE(EOS(STATIC_496), i13, i125, i125) → 500_0_test_LE(EOS(STATIC_500), i13, i125, i125)
499_0_test_LE(EOS(STATIC_499), i13, matching1, matching2) → 502_0_test_Load(EOS(STATIC_502), i13) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
500_0_test_LE(EOS(STATIC_500), i13, i125, i125) → 504_0_test_Inc(EOS(STATIC_504), i13, i125) | >(i125, 0)
502_0_test_Load(EOS(STATIC_502), i13) → 507_0_test_Store(EOS(STATIC_507), i13, i13)
504_0_test_Inc(EOS(STATIC_504), i13, i125) → 509_0_test_JMP(EOS(STATIC_509), i13, +(i125, -1)) | >(i125, 0)
507_0_test_Store(EOS(STATIC_507), i13, i13) → 511_0_test_Load(EOS(STATIC_511), i13, i13)
509_0_test_JMP(EOS(STATIC_509), i13, i127) → 514_0_test_Load(EOS(STATIC_514), i13, i127)
511_0_test_Load(EOS(STATIC_511), i13, i13) → 525_0_test_Load(EOS(STATIC_525), i13, i13)
514_0_test_Load(EOS(STATIC_514), i13, i127) → 493_0_test_Load(EOS(STATIC_493), i13, i127)
525_0_test_Load(EOS(STATIC_525), i13, i131) → 528_0_test_LE(EOS(STATIC_528), i13, i131, i131)
528_0_test_LE(EOS(STATIC_528), i13, matching1, matching2) → 530_0_test_LE(EOS(STATIC_530), i13, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
528_0_test_LE(EOS(STATIC_528), i13, i136, i136) → 531_0_test_LE(EOS(STATIC_531), i13, i136, i136)
530_0_test_LE(EOS(STATIC_530), i13, matching1, matching2) → 533_0_test_Load(EOS(STATIC_533), i13) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
531_0_test_LE(EOS(STATIC_531), i13, i136, i136) → 535_0_test_Inc(EOS(STATIC_535), i13, i136) | >(i136, 0)
533_0_test_Load(EOS(STATIC_533), i13) → 536_0_test_Store(EOS(STATIC_536), i13, i13)
535_0_test_Inc(EOS(STATIC_535), i13, i136) → 539_0_test_JMP(EOS(STATIC_539), i13, +(i136, -1)) | >(i136, 0)
536_0_test_Store(EOS(STATIC_536), i13, i13) → 540_0_test_Load(EOS(STATIC_540), i13, i13)
539_0_test_JMP(EOS(STATIC_539), i13, i138) → 545_0_test_Load(EOS(STATIC_545), i13, i138)
540_0_test_Load(EOS(STATIC_540), i13, i13) → 561_0_test_Load(EOS(STATIC_561), i13, i13)
545_0_test_Load(EOS(STATIC_545), i13, i138) → 525_0_test_Load(EOS(STATIC_525), i13, i138)
561_0_test_Load(EOS(STATIC_561), i13, i143) → 564_0_test_LE(EOS(STATIC_564), i13, i143, i143)
564_0_test_LE(EOS(STATIC_564), i13, matching1, matching2) → 566_0_test_LE(EOS(STATIC_566), i13, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
564_0_test_LE(EOS(STATIC_564), i13, i148, i148) → 568_0_test_LE(EOS(STATIC_568), i13, i148, i148)
566_0_test_LE(EOS(STATIC_566), i13, matching1, matching2) → 570_0_test_Load(EOS(STATIC_570), i13) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
568_0_test_LE(EOS(STATIC_568), i13, i148, i148) → 572_0_test_Inc(EOS(STATIC_572), i13, i148) | >(i148, 0)
570_0_test_Load(EOS(STATIC_570), i13) → 574_0_test_Store(EOS(STATIC_574), i13, i13)
572_0_test_Inc(EOS(STATIC_572), i13, i148) → 577_0_test_JMP(EOS(STATIC_577), i13, +(i148, -1)) | >(i148, 0)
574_0_test_Store(EOS(STATIC_574), i13, i13) → 579_0_test_Load(EOS(STATIC_579), i13, i13)
577_0_test_JMP(EOS(STATIC_577), i13, i151) → 583_0_test_Load(EOS(STATIC_583), i13, i151)
579_0_test_Load(EOS(STATIC_579), i13, i13) → 598_0_test_Load(EOS(STATIC_598), i13, i13)
583_0_test_Load(EOS(STATIC_583), i13, i151) → 561_0_test_Load(EOS(STATIC_561), i13, i151)
598_0_test_Load(EOS(STATIC_598), i13, i157) → 602_0_test_LE(EOS(STATIC_602), i13, i157, i157)
602_0_test_LE(EOS(STATIC_602), i13, matching1, matching2) → 604_0_test_LE(EOS(STATIC_604), i13, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
602_0_test_LE(EOS(STATIC_602), i13, i161, i161) → 606_0_test_LE(EOS(STATIC_606), i13, i161, i161)
604_0_test_LE(EOS(STATIC_604), i13, matching1, matching2) → 608_0_test_Load(EOS(STATIC_608), i13) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
606_0_test_LE(EOS(STATIC_606), i13, i161, i161) → 610_0_test_Inc(EOS(STATIC_610), i13, i161) | >(i161, 0)
608_0_test_Load(EOS(STATIC_608), i13) → 612_0_test_Store(EOS(STATIC_612), i13, i13)
610_0_test_Inc(EOS(STATIC_610), i13, i161) → 614_0_test_JMP(EOS(STATIC_614), i13, +(i161, -1)) | >(i161, 0)
612_0_test_Store(EOS(STATIC_612), i13, i13) → 617_0_test_Load(EOS(STATIC_617), i13, i13)
614_0_test_JMP(EOS(STATIC_614), i13, i163) → 621_0_test_Load(EOS(STATIC_621), i13, i163)
617_0_test_Load(EOS(STATIC_617), i13, i13) → 637_0_test_Load(EOS(STATIC_637), i13, i13)
621_0_test_Load(EOS(STATIC_621), i13, i163) → 598_0_test_Load(EOS(STATIC_598), i13, i163)
637_0_test_Load(EOS(STATIC_637), i13, i169) → 641_0_test_LE(EOS(STATIC_641), i13, i169, i169)
641_0_test_LE(EOS(STATIC_641), i13, matching1, matching2) → 643_0_test_LE(EOS(STATIC_643), i13, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
641_0_test_LE(EOS(STATIC_641), i13, i173, i173) → 645_0_test_LE(EOS(STATIC_645), i13, i173, i173)
643_0_test_LE(EOS(STATIC_643), i13, matching1, matching2) → 647_0_test_Load(EOS(STATIC_647), i13) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
645_0_test_LE(EOS(STATIC_645), i13, i173, i173) → 649_0_test_Inc(EOS(STATIC_649), i13, i173) | >(i173, 0)
647_0_test_Load(EOS(STATIC_647), i13) → 651_0_test_Store(EOS(STATIC_651), i13, i13)
649_0_test_Inc(EOS(STATIC_649), i13, i173) → 654_0_test_JMP(EOS(STATIC_654), i13, +(i173, -1)) | >(i173, 0)
651_0_test_Store(EOS(STATIC_651), i13, i13) → 656_0_test_Load(EOS(STATIC_656), i13, i13)
654_0_test_JMP(EOS(STATIC_654), i13, i177) → 660_0_test_Load(EOS(STATIC_660), i13, i177)
656_0_test_Load(EOS(STATIC_656), i13, i13) → 676_0_test_Load(EOS(STATIC_676), i13, i13)
660_0_test_Load(EOS(STATIC_660), i13, i177) → 637_0_test_Load(EOS(STATIC_637), i13, i177)
676_0_test_Load(EOS(STATIC_676), i13, i184) → 680_0_test_LE(EOS(STATIC_680), i13, i184, i184)
680_0_test_LE(EOS(STATIC_680), i13, matching1, matching2) → 682_0_test_LE(EOS(STATIC_682), i13, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
680_0_test_LE(EOS(STATIC_680), i13, i189, i189) → 683_0_test_LE(EOS(STATIC_683), i13, i189, i189)
682_0_test_LE(EOS(STATIC_682), i13, matching1, matching2) → 686_0_test_Load(EOS(STATIC_686), i13) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
683_0_test_LE(EOS(STATIC_683), i13, i189, i189) → 688_0_test_Inc(EOS(STATIC_688), i13, i189) | >(i189, 0)
686_0_test_Load(EOS(STATIC_686), i13) → 690_0_test_Store(EOS(STATIC_690), i13, i13)
688_0_test_Inc(EOS(STATIC_688), i13, i189) → 692_0_test_JMP(EOS(STATIC_692), i13, +(i189, -1)) | >(i189, 0)
690_0_test_Store(EOS(STATIC_690), i13, i13) → 695_0_test_Load(EOS(STATIC_695), i13, i13)
692_0_test_JMP(EOS(STATIC_692), i13, i191) → 699_0_test_Load(EOS(STATIC_699), i13, i191)
695_0_test_Load(EOS(STATIC_695), i13, i13) → 713_0_test_Load(EOS(STATIC_713), i13, i13)
699_0_test_Load(EOS(STATIC_699), i13, i191) → 676_0_test_Load(EOS(STATIC_676), i13, i191)
713_0_test_Load(EOS(STATIC_713), i13, i194) → 715_0_test_LE(EOS(STATIC_715), i13, i194, i194)
715_0_test_LE(EOS(STATIC_715), i13, matching1, matching2) → 717_0_test_LE(EOS(STATIC_717), i13, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
715_0_test_LE(EOS(STATIC_715), i13, i197, i197) → 718_0_test_LE(EOS(STATIC_718), i13, i197, i197)
717_0_test_LE(EOS(STATIC_717), i13, matching1, matching2) → 720_0_test_Load(EOS(STATIC_720), i13) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
718_0_test_LE(EOS(STATIC_718), i13, i197, i197) → 722_0_test_Inc(EOS(STATIC_722), i13, i197) | >(i197, 0)
720_0_test_Load(EOS(STATIC_720), i13) → 724_0_test_Store(EOS(STATIC_724), i13)
722_0_test_Inc(EOS(STATIC_722), i13, i197) → 726_0_test_JMP(EOS(STATIC_726), i13, +(i197, -1)) | >(i197, 0)
724_0_test_Store(EOS(STATIC_724), i13) → 728_0_test_Load(EOS(STATIC_728), i13)
726_0_test_JMP(EOS(STATIC_726), i13, i199) → 731_0_test_Load(EOS(STATIC_731), i13, i199)
728_0_test_Load(EOS(STATIC_728), i13) → 744_0_test_Load(EOS(STATIC_744), i13)
731_0_test_Load(EOS(STATIC_731), i13, i199) → 713_0_test_Load(EOS(STATIC_713), i13, i199)
744_0_test_Load(EOS(STATIC_744), i203) → 746_0_test_LE(EOS(STATIC_746), i203, i203)
746_0_test_LE(EOS(STATIC_746), matching1, matching2) → 748_0_test_LE(EOS(STATIC_748), 0, 0) | &&(=(matching1, 0), =(matching2, 0))
746_0_test_LE(EOS(STATIC_746), i208, i208) → 750_0_test_LE(EOS(STATIC_750), i208, i208)
748_0_test_LE(EOS(STATIC_748), matching1, matching2) → 751_0_test_Return(EOS(STATIC_751)) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
750_0_test_LE(EOS(STATIC_750), i208, i208) → 753_0_test_Inc(EOS(STATIC_753), i208) | >(i208, 0)
753_0_test_Inc(EOS(STATIC_753), i208) → 759_0_test_JMP(EOS(STATIC_759), +(i208, -1)) | >(i208, 0)
759_0_test_JMP(EOS(STATIC_759), i211) → 770_0_test_Load(EOS(STATIC_770), i211)
770_0_test_Load(EOS(STATIC_770), i211) → 744_0_test_Load(EOS(STATIC_744), i211)
Combined rules. Obtained 3 conditional rules for P and 25 conditional rules for R.
P rules:
90_0_main_GE(EOS(STATIC_90), x0, x1, x1, 100) → 97_1_main_InvokeMethod(97_0_test_Load(EOS(STATIC_97), x1), x0, x1, x1) | <(x1, 100)
97_1_main_InvokeMethod(751_0_test_Return(EOS(STATIC_751)), x0, x1, x1) → 90_0_main_GE(EOS(STATIC_90), x0, +(x1, 1), +(x1, 1), 100) | >(x1, 0)
90_0_main_GE(EOS(STATIC_90), x0, x1, x1, 100) → 90_0_main_GE(EOS(STATIC_90), -(x0, 1), -(x0, 1), -(x0, 1), 100) | &&(>(+(x1, 1), 100), >(x0, 1))
R rules:
97_0_test_Load(EOS(STATIC_97), x0) → 356_0_test_LE(EOS(STATIC_356), x0, x0, x0)
356_0_test_LE(EOS(STATIC_356), x0, x1, x1) → 356_0_test_LE(EOS(STATIC_356), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
356_0_test_LE(EOS(STATIC_356), x0, 0, 0) → 389_0_test_LE(EOS(STATIC_389), x0, x0, x0)
389_0_test_LE(EOS(STATIC_389), x0, x1, x1) → 389_0_test_LE(EOS(STATIC_389), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
389_0_test_LE(EOS(STATIC_389), x0, 0, 0) → 416_0_test_LE(EOS(STATIC_416), x0, x0, x0)
416_0_test_LE(EOS(STATIC_416), x0, x1, x1) → 416_0_test_LE(EOS(STATIC_416), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
416_0_test_LE(EOS(STATIC_416), x0, 0, 0) → 456_0_test_LE(EOS(STATIC_456), x0, x0, x0)
456_0_test_LE(EOS(STATIC_456), x0, x1, x1) → 456_0_test_LE(EOS(STATIC_456), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
456_0_test_LE(EOS(STATIC_456), x0, 0, 0) → 496_0_test_LE(EOS(STATIC_496), x0, x0, x0)
496_0_test_LE(EOS(STATIC_496), x0, x1, x1) → 496_0_test_LE(EOS(STATIC_496), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
496_0_test_LE(EOS(STATIC_496), x0, 0, 0) → 528_0_test_LE(EOS(STATIC_528), x0, x0, x0)
528_0_test_LE(EOS(STATIC_528), x0, x1, x1) → 528_0_test_LE(EOS(STATIC_528), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
528_0_test_LE(EOS(STATIC_528), x0, 0, 0) → 564_0_test_LE(EOS(STATIC_564), x0, x0, x0)
564_0_test_LE(EOS(STATIC_564), x0, x1, x1) → 564_0_test_LE(EOS(STATIC_564), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
564_0_test_LE(EOS(STATIC_564), x0, 0, 0) → 602_0_test_LE(EOS(STATIC_602), x0, x0, x0)
602_0_test_LE(EOS(STATIC_602), x0, x1, x1) → 602_0_test_LE(EOS(STATIC_602), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
602_0_test_LE(EOS(STATIC_602), x0, 0, 0) → 641_0_test_LE(EOS(STATIC_641), x0, x0, x0)
641_0_test_LE(EOS(STATIC_641), x0, x1, x1) → 641_0_test_LE(EOS(STATIC_641), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
641_0_test_LE(EOS(STATIC_641), x0, 0, 0) → 680_0_test_LE(EOS(STATIC_680), x0, x0, x0)
680_0_test_LE(EOS(STATIC_680), x0, x1, x1) → 680_0_test_LE(EOS(STATIC_680), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
680_0_test_LE(EOS(STATIC_680), x0, 0, 0) → 715_0_test_LE(EOS(STATIC_715), x0, x0, x0)
715_0_test_LE(EOS(STATIC_715), x0, x1, x1) → 715_0_test_LE(EOS(STATIC_715), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
715_0_test_LE(EOS(STATIC_715), x0, 0, 0) → 746_0_test_LE(EOS(STATIC_746), x0, x0)
746_0_test_LE(EOS(STATIC_746), 0, 0) → 751_0_test_Return(EOS(STATIC_751))
746_0_test_LE(EOS(STATIC_746), x0, x0) → 746_0_test_LE(EOS(STATIC_746), +(x0, -1), +(x0, -1)) | >(x0, 0)
Filtered ground terms:
90_0_main_GE(x1, x2, x3, x4, x5) → 90_0_main_GE(x2, x3, x4)
Cond_90_0_main_GE1(x1, x2, x3, x4, x5, x6) → Cond_90_0_main_GE1(x1, x3, x4, x5)
Cond_97_1_main_InvokeMethod(x1, x2, x3, x4, x5) → Cond_97_1_main_InvokeMethod(x1, x3, x4, x5)
751_0_test_Return(x1) → 751_0_test_Return
97_0_test_Load(x1, x2) → 97_0_test_Load(x2)
Cond_90_0_main_GE(x1, x2, x3, x4, x5, x6) → Cond_90_0_main_GE(x1, x3, x4, x5)
746_0_test_LE(x1, x2, x3) → 746_0_test_LE(x2, x3)
Cond_746_0_test_LE(x1, x2, x3, x4) → Cond_746_0_test_LE(x1, x3, x4)
715_0_test_LE(x1, x2, x3, x4) → 715_0_test_LE(x2, x3, x4)
Cond_715_0_test_LE(x1, x2, x3, x4, x5) → Cond_715_0_test_LE(x1, x3, x4, x5)
680_0_test_LE(x1, x2, x3, x4) → 680_0_test_LE(x2, x3, x4)
Cond_680_0_test_LE(x1, x2, x3, x4, x5) → Cond_680_0_test_LE(x1, x3, x4, x5)
641_0_test_LE(x1, x2, x3, x4) → 641_0_test_LE(x2, x3, x4)
Cond_641_0_test_LE(x1, x2, x3, x4, x5) → Cond_641_0_test_LE(x1, x3, x4, x5)
602_0_test_LE(x1, x2, x3, x4) → 602_0_test_LE(x2, x3, x4)
Cond_602_0_test_LE(x1, x2, x3, x4, x5) → Cond_602_0_test_LE(x1, x3, x4, x5)
564_0_test_LE(x1, x2, x3, x4) → 564_0_test_LE(x2, x3, x4)
Cond_564_0_test_LE(x1, x2, x3, x4, x5) → Cond_564_0_test_LE(x1, x3, x4, x5)
528_0_test_LE(x1, x2, x3, x4) → 528_0_test_LE(x2, x3, x4)
Cond_528_0_test_LE(x1, x2, x3, x4, x5) → Cond_528_0_test_LE(x1, x3, x4, x5)
496_0_test_LE(x1, x2, x3, x4) → 496_0_test_LE(x2, x3, x4)
Cond_496_0_test_LE(x1, x2, x3, x4, x5) → Cond_496_0_test_LE(x1, x3, x4, x5)
456_0_test_LE(x1, x2, x3, x4) → 456_0_test_LE(x2, x3, x4)
Cond_456_0_test_LE(x1, x2, x3, x4, x5) → Cond_456_0_test_LE(x1, x3, x4, x5)
416_0_test_LE(x1, x2, x3, x4) → 416_0_test_LE(x2, x3, x4)
Cond_416_0_test_LE(x1, x2, x3, x4, x5) → Cond_416_0_test_LE(x1, x3, x4, x5)
389_0_test_LE(x1, x2, x3, x4) → 389_0_test_LE(x2, x3, x4)
Cond_389_0_test_LE(x1, x2, x3, x4, x5) → Cond_389_0_test_LE(x1, x3, x4, x5)
356_0_test_LE(x1, x2, x3, x4) → 356_0_test_LE(x2, x3, x4)
Cond_356_0_test_LE(x1, x2, x3, x4, x5) → Cond_356_0_test_LE(x1, x3, x4, x5)
Filtered duplicate args:
90_0_main_GE(x1, x2, x3) → 90_0_main_GE(x1, x3)
Cond_90_0_main_GE(x1, x2, x3, x4) → Cond_90_0_main_GE(x1, x2, x4)
97_1_main_InvokeMethod(x1, x2, x3, x4) → 97_1_main_InvokeMethod(x1, x2, x4)
Cond_97_1_main_InvokeMethod(x1, x2, x3, x4) → Cond_97_1_main_InvokeMethod(x1, x2, x4)
Cond_90_0_main_GE1(x1, x2, x3, x4) → Cond_90_0_main_GE1(x1, x2, x4)
Cond_356_0_test_LE(x1, x2, x3, x4) → Cond_356_0_test_LE(x1, x2, x4)
Cond_389_0_test_LE(x1, x2, x3, x4) → Cond_389_0_test_LE(x1, x2, x4)
Cond_416_0_test_LE(x1, x2, x3, x4) → Cond_416_0_test_LE(x1, x2, x4)
Cond_456_0_test_LE(x1, x2, x3, x4) → Cond_456_0_test_LE(x1, x2, x4)
Cond_496_0_test_LE(x1, x2, x3, x4) → Cond_496_0_test_LE(x1, x2, x4)
Cond_528_0_test_LE(x1, x2, x3, x4) → Cond_528_0_test_LE(x1, x2, x4)
Cond_564_0_test_LE(x1, x2, x3, x4) → Cond_564_0_test_LE(x1, x2, x4)
Cond_602_0_test_LE(x1, x2, x3, x4) → Cond_602_0_test_LE(x1, x2, x4)
Cond_641_0_test_LE(x1, x2, x3, x4) → Cond_641_0_test_LE(x1, x2, x4)
Cond_680_0_test_LE(x1, x2, x3, x4) → Cond_680_0_test_LE(x1, x2, x4)
Cond_715_0_test_LE(x1, x2, x3, x4) → Cond_715_0_test_LE(x1, x2, x4)
746_0_test_LE(x1, x2) → 746_0_test_LE(x2)
Cond_746_0_test_LE(x1, x2, x3) → Cond_746_0_test_LE(x1, x3)
Filtered unneeded arguments:
Cond_90_0_main_GE1(x1, x2, x3) → Cond_90_0_main_GE1(x1, x2)
Combined rules. Obtained 3 conditional rules for P and 25 conditional rules for R.
P rules:
90_0_main_GE(x0, x1) → 97_1_main_InvokeMethod(97_0_test_Load(x1), x0, x1) | <(x1, 100)
97_1_main_InvokeMethod(751_0_test_Return, x0, x1) → 90_0_main_GE(x0, +(x1, 1)) | >(x1, 0)
90_0_main_GE(x0, x1) → 90_0_main_GE(-(x0, 1), -(x0, 1)) | &&(>(x1, 99), >(x0, 1))
R rules:
97_0_test_Load(x0) → 356_0_test_LE(x0, x0, x0)
356_0_test_LE(x0, x1, x1) → 356_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
356_0_test_LE(x0, 0, 0) → 389_0_test_LE(x0, x0, x0)
389_0_test_LE(x0, x1, x1) → 389_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
389_0_test_LE(x0, 0, 0) → 416_0_test_LE(x0, x0, x0)
416_0_test_LE(x0, x1, x1) → 416_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
416_0_test_LE(x0, 0, 0) → 456_0_test_LE(x0, x0, x0)
456_0_test_LE(x0, x1, x1) → 456_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
456_0_test_LE(x0, 0, 0) → 496_0_test_LE(x0, x0, x0)
496_0_test_LE(x0, x1, x1) → 496_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
496_0_test_LE(x0, 0, 0) → 528_0_test_LE(x0, x0, x0)
528_0_test_LE(x0, x1, x1) → 528_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
528_0_test_LE(x0, 0, 0) → 564_0_test_LE(x0, x0, x0)
564_0_test_LE(x0, x1, x1) → 564_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
564_0_test_LE(x0, 0, 0) → 602_0_test_LE(x0, x0, x0)
602_0_test_LE(x0, x1, x1) → 602_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
602_0_test_LE(x0, 0, 0) → 641_0_test_LE(x0, x0, x0)
641_0_test_LE(x0, x1, x1) → 641_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
641_0_test_LE(x0, 0, 0) → 680_0_test_LE(x0, x0, x0)
680_0_test_LE(x0, x1, x1) → 680_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
680_0_test_LE(x0, 0, 0) → 715_0_test_LE(x0, x0, x0)
715_0_test_LE(x0, x1, x1) → 715_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
715_0_test_LE(x0, 0, 0) → 746_0_test_LE(x0)
746_0_test_LE(0) → 751_0_test_Return
746_0_test_LE(x0) → 746_0_test_LE(+(x0, -1)) | >(x0, 0)
Finished conversion. Obtained 6 rules for P and 37 rules for R. System has predefined symbols.
P rules:
90_0_MAIN_GE(x0, x1) → COND_90_0_MAIN_GE(<(x1, 100), x0, x1)
COND_90_0_MAIN_GE(TRUE, x0, x1) → 97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1), x0, x1)
97_1_MAIN_INVOKEMETHOD(751_0_test_Return, x0, x1) → COND_97_1_MAIN_INVOKEMETHOD(>(x1, 0), 751_0_test_Return, x0, x1)
COND_97_1_MAIN_INVOKEMETHOD(TRUE, 751_0_test_Return, x0, x1) → 90_0_MAIN_GE(x0, +(x1, 1))
90_0_MAIN_GE(x0, x1) → COND_90_0_MAIN_GE1(&&(>(x1, 99), >(x0, 1)), x0, x1)
COND_90_0_MAIN_GE1(TRUE, x0, x1) → 90_0_MAIN_GE(-(x0, 1), -(x0, 1))
R rules:
97_0_test_Load(x0) → 356_0_test_LE(x0, x0, x0)
356_0_test_LE(x0, x1, x1) → Cond_356_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_356_0_test_LE(TRUE, x0, x1, x1) → 356_0_test_LE(x0, +(x1, -1), +(x1, -1))
356_0_test_LE(x0, 0, 0) → 389_0_test_LE(x0, x0, x0)
389_0_test_LE(x0, x1, x1) → Cond_389_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_389_0_test_LE(TRUE, x0, x1, x1) → 389_0_test_LE(x0, +(x1, -1), +(x1, -1))
389_0_test_LE(x0, 0, 0) → 416_0_test_LE(x0, x0, x0)
416_0_test_LE(x0, x1, x1) → Cond_416_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_416_0_test_LE(TRUE, x0, x1, x1) → 416_0_test_LE(x0, +(x1, -1), +(x1, -1))
416_0_test_LE(x0, 0, 0) → 456_0_test_LE(x0, x0, x0)
456_0_test_LE(x0, x1, x1) → Cond_456_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_456_0_test_LE(TRUE, x0, x1, x1) → 456_0_test_LE(x0, +(x1, -1), +(x1, -1))
456_0_test_LE(x0, 0, 0) → 496_0_test_LE(x0, x0, x0)
496_0_test_LE(x0, x1, x1) → Cond_496_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_496_0_test_LE(TRUE, x0, x1, x1) → 496_0_test_LE(x0, +(x1, -1), +(x1, -1))
496_0_test_LE(x0, 0, 0) → 528_0_test_LE(x0, x0, x0)
528_0_test_LE(x0, x1, x1) → Cond_528_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_528_0_test_LE(TRUE, x0, x1, x1) → 528_0_test_LE(x0, +(x1, -1), +(x1, -1))
528_0_test_LE(x0, 0, 0) → 564_0_test_LE(x0, x0, x0)
564_0_test_LE(x0, x1, x1) → Cond_564_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_564_0_test_LE(TRUE, x0, x1, x1) → 564_0_test_LE(x0, +(x1, -1), +(x1, -1))
564_0_test_LE(x0, 0, 0) → 602_0_test_LE(x0, x0, x0)
602_0_test_LE(x0, x1, x1) → Cond_602_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_602_0_test_LE(TRUE, x0, x1, x1) → 602_0_test_LE(x0, +(x1, -1), +(x1, -1))
602_0_test_LE(x0, 0, 0) → 641_0_test_LE(x0, x0, x0)
641_0_test_LE(x0, x1, x1) → Cond_641_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_641_0_test_LE(TRUE, x0, x1, x1) → 641_0_test_LE(x0, +(x1, -1), +(x1, -1))
641_0_test_LE(x0, 0, 0) → 680_0_test_LE(x0, x0, x0)
680_0_test_LE(x0, x1, x1) → Cond_680_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_680_0_test_LE(TRUE, x0, x1, x1) → 680_0_test_LE(x0, +(x1, -1), +(x1, -1))
680_0_test_LE(x0, 0, 0) → 715_0_test_LE(x0, x0, x0)
715_0_test_LE(x0, x1, x1) → Cond_715_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_715_0_test_LE(TRUE, x0, x1, x1) → 715_0_test_LE(x0, +(x1, -1), +(x1, -1))
715_0_test_LE(x0, 0, 0) → 746_0_test_LE(x0)
746_0_test_LE(0) → 751_0_test_Return
746_0_test_LE(x0) → Cond_746_0_test_LE(>(x0, 0), x0)
Cond_746_0_test_LE(TRUE, x0) → 746_0_test_LE(+(x0, -1))
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
(0) -> (1), if (x1[0] < 100 ∧x0[0] →* x0[1]∧x1[0] →* x1[1])
(1) -> (2), if (97_0_test_Load(x1[1]) →* 751_0_test_Return∧x0[1] →* x0[2]∧x1[1] →* x1[2])
(2) -> (3), if (x1[2] > 0 ∧x0[2] →* x0[3]∧x1[2] →* x1[3])
(3) -> (0), if (x0[3] →* x0[0]∧x1[3] + 1 →* x1[0])
(3) -> (4), if (x0[3] →* x0[4]∧x1[3] + 1 →* x1[4])
(4) -> (5), if (x1[4] > 99 && x0[4] > 1 ∧x0[4] →* x0[5]∧x1[4] →* x1[5])
(5) -> (0), if (x0[5] - 1 →* x0[0]∧x0[5] - 1 →* x1[0])
(5) -> (4), if (x0[5] - 1 →* x0[4]∧x0[5] - 1 →* x1[4])
(1) (<(x1[0], 100)=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1] ⇒ 90_0_MAIN_GE(x0[0], x1[0])≥NonInfC∧90_0_MAIN_GE(x0[0], x1[0])≥COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])∧(UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥))
(2) (<(x1[0], 100)=TRUE ⇒ 90_0_MAIN_GE(x0[0], x1[0])≥NonInfC∧90_0_MAIN_GE(x0[0], x1[0])≥COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])∧(UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥))
(3) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_87 + (-1)Bound*bni_87] + [bni_87]x0[0] ≥ 0∧[(-1)bso_88] ≥ 0)
(4) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_87 + (-1)Bound*bni_87] + [bni_87]x0[0] ≥ 0∧[(-1)bso_88] ≥ 0)
(5) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_87 + (-1)Bound*bni_87] + [bni_87]x0[0] ≥ 0∧[(-1)bso_88] ≥ 0)
(6) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[bni_87] = 0∧[(-1)bni_87 + (-1)Bound*bni_87] ≥ 0∧0 = 0∧[(-1)bso_88] ≥ 0)
(7) ([99] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[bni_87] = 0∧[(-1)bni_87 + (-1)Bound*bni_87] ≥ 0∧0 = 0∧[(-1)bso_88] ≥ 0)
(8) ([99] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[bni_87] = 0∧[(-1)bni_87 + (-1)Bound*bni_87] ≥ 0∧0 = 0∧[(-1)bso_88] ≥ 0)
(9) (COND_90_0_MAIN_GE(TRUE, x0[1], x1[1])≥NonInfC∧COND_90_0_MAIN_GE(TRUE, x0[1], x1[1])≥97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1[1]), x0[1], x1[1])∧(UIncreasing(97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1[1]), x0[1], x1[1])), ≥))
(10) ((UIncreasing(97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_89] = 0∧[(-1)bso_90] ≥ 0)
(11) ((UIncreasing(97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_89] = 0∧[(-1)bso_90] ≥ 0)
(12) ((UIncreasing(97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_89] = 0∧[(-1)bso_90] ≥ 0)
(13) ((UIncreasing(97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_89] = 0∧0 = 0∧0 = 0∧[(-1)bso_90] ≥ 0)
(14) (>(x1[2], 0)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3] ⇒ 97_1_MAIN_INVOKEMETHOD(751_0_test_Return, x0[2], x1[2])≥NonInfC∧97_1_MAIN_INVOKEMETHOD(751_0_test_Return, x0[2], x1[2])≥COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])∧(UIncreasing(COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])), ≥))
(15) (>(x1[2], 0)=TRUE ⇒ 97_1_MAIN_INVOKEMETHOD(751_0_test_Return, x0[2], x1[2])≥NonInfC∧97_1_MAIN_INVOKEMETHOD(751_0_test_Return, x0[2], x1[2])≥COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])∧(UIncreasing(COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])), ≥))
(16) (x1[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])), ≥)∧[(-1)bni_91 + (-1)Bound*bni_91] + [bni_91]x0[2] ≥ 0∧[(-1)bso_92] ≥ 0)
(17) (x1[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])), ≥)∧[(-1)bni_91 + (-1)Bound*bni_91] + [bni_91]x0[2] ≥ 0∧[(-1)bso_92] ≥ 0)
(18) (x1[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])), ≥)∧[(-1)bni_91 + (-1)Bound*bni_91] + [bni_91]x0[2] ≥ 0∧[(-1)bso_92] ≥ 0)
(19) (x1[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])), ≥)∧[bni_91] = 0∧[(-1)bni_91 + (-1)Bound*bni_91] ≥ 0∧0 = 0∧[(-1)bso_92] ≥ 0)
(20) (x1[2] ≥ 0 ⇒ (UIncreasing(COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])), ≥)∧[bni_91] = 0∧[(-1)bni_91 + (-1)Bound*bni_91] ≥ 0∧0 = 0∧[(-1)bso_92] ≥ 0)
(21) (COND_97_1_MAIN_INVOKEMETHOD(TRUE, 751_0_test_Return, x0[3], x1[3])≥NonInfC∧COND_97_1_MAIN_INVOKEMETHOD(TRUE, 751_0_test_Return, x0[3], x1[3])≥90_0_MAIN_GE(x0[3], +(x1[3], 1))∧(UIncreasing(90_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥))
(22) ((UIncreasing(90_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_93] = 0∧[(-1)bso_94] ≥ 0)
(23) ((UIncreasing(90_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_93] = 0∧[(-1)bso_94] ≥ 0)
(24) ((UIncreasing(90_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_93] = 0∧[(-1)bso_94] ≥ 0)
(25) ((UIncreasing(90_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_93] = 0∧0 = 0∧0 = 0∧[(-1)bso_94] ≥ 0)
(26) (&&(>(x1[4], 99), >(x0[4], 1))=TRUE∧x0[4]=x0[5]∧x1[4]=x1[5] ⇒ 90_0_MAIN_GE(x0[4], x1[4])≥NonInfC∧90_0_MAIN_GE(x0[4], x1[4])≥COND_90_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])∧(UIncreasing(COND_90_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])), ≥))
(27) (>(x1[4], 99)=TRUE∧>(x0[4], 1)=TRUE ⇒ 90_0_MAIN_GE(x0[4], x1[4])≥NonInfC∧90_0_MAIN_GE(x0[4], x1[4])≥COND_90_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])∧(UIncreasing(COND_90_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])), ≥))
(28) (x1[4] + [-100] ≥ 0∧x0[4] + [-2] ≥ 0 ⇒ (UIncreasing(COND_90_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])), ≥)∧[(-1)bni_95 + (-1)Bound*bni_95] + [bni_95]x0[4] ≥ 0∧[(-1)bso_96] ≥ 0)
(29) (x1[4] + [-100] ≥ 0∧x0[4] + [-2] ≥ 0 ⇒ (UIncreasing(COND_90_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])), ≥)∧[(-1)bni_95 + (-1)Bound*bni_95] + [bni_95]x0[4] ≥ 0∧[(-1)bso_96] ≥ 0)
(30) (x1[4] + [-100] ≥ 0∧x0[4] + [-2] ≥ 0 ⇒ (UIncreasing(COND_90_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])), ≥)∧[(-1)bni_95 + (-1)Bound*bni_95] + [bni_95]x0[4] ≥ 0∧[(-1)bso_96] ≥ 0)
(31) (x1[4] ≥ 0∧x0[4] + [-2] ≥ 0 ⇒ (UIncreasing(COND_90_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])), ≥)∧[(-1)bni_95 + (-1)Bound*bni_95] + [bni_95]x0[4] ≥ 0∧[(-1)bso_96] ≥ 0)
(32) (x1[4] ≥ 0∧x0[4] ≥ 0 ⇒ (UIncreasing(COND_90_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])), ≥)∧[bni_95 + (-1)Bound*bni_95] + [bni_95]x0[4] ≥ 0∧[(-1)bso_96] ≥ 0)
(33) (COND_90_0_MAIN_GE1(TRUE, x0[5], x1[5])≥NonInfC∧COND_90_0_MAIN_GE1(TRUE, x0[5], x1[5])≥90_0_MAIN_GE(-(x0[5], 1), -(x0[5], 1))∧(UIncreasing(90_0_MAIN_GE(-(x0[5], 1), -(x0[5], 1))), ≥))
(34) ((UIncreasing(90_0_MAIN_GE(-(x0[5], 1), -(x0[5], 1))), ≥)∧[bni_97] = 0∧[1 + (-1)bso_98] ≥ 0)
(35) ((UIncreasing(90_0_MAIN_GE(-(x0[5], 1), -(x0[5], 1))), ≥)∧[bni_97] = 0∧[1 + (-1)bso_98] ≥ 0)
(36) ((UIncreasing(90_0_MAIN_GE(-(x0[5], 1), -(x0[5], 1))), ≥)∧[bni_97] = 0∧[1 + (-1)bso_98] ≥ 0)
(37) ((UIncreasing(90_0_MAIN_GE(-(x0[5], 1), -(x0[5], 1))), ≥)∧[bni_97] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_98] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(97_0_test_Load(x1)) = [1]
POL(356_0_test_LE(x1, x2, x3)) = [1] + x3 + [-1]x2
POL(Cond_356_0_test_LE(x1, x2, x3, x4)) = [1] + [-1]x4 + x3
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(389_0_test_LE(x1, x2, x3)) = [1] + x3 + [-1]x2
POL(Cond_389_0_test_LE(x1, x2, x3, x4)) = [1] + [-1]x4 + x3
POL(416_0_test_LE(x1, x2, x3)) = [1] + x3 + [-1]x2
POL(Cond_416_0_test_LE(x1, x2, x3, x4)) = [1] + [-1]x4 + x3
POL(456_0_test_LE(x1, x2, x3)) = [1] + x3 + [-1]x2
POL(Cond_456_0_test_LE(x1, x2, x3, x4)) = [1] + [-1]x4 + x3
POL(496_0_test_LE(x1, x2, x3)) = [1] + x3 + [-1]x2
POL(Cond_496_0_test_LE(x1, x2, x3, x4)) = [1] + [-1]x4 + x3
POL(528_0_test_LE(x1, x2, x3)) = [1] + x3 + [-1]x2
POL(Cond_528_0_test_LE(x1, x2, x3, x4)) = [1] + [-1]x4 + x3
POL(564_0_test_LE(x1, x2, x3)) = [1] + x3 + [-1]x2
POL(Cond_564_0_test_LE(x1, x2, x3, x4)) = [1] + [-1]x4 + x3
POL(602_0_test_LE(x1, x2, x3)) = [1]
POL(Cond_602_0_test_LE(x1, x2, x3, x4)) = [1]
POL(641_0_test_LE(x1, x2, x3)) = [1] + x3 + [-1]x2
POL(Cond_641_0_test_LE(x1, x2, x3, x4)) = [1] + [-1]x4 + x3
POL(680_0_test_LE(x1, x2, x3)) = [1] + x3 + [-1]x2
POL(Cond_680_0_test_LE(x1, x2, x3, x4)) = [1] + [-1]x4 + x3
POL(715_0_test_LE(x1, x2, x3)) = [1] + x3 + [-1]x2
POL(Cond_715_0_test_LE(x1, x2, x3, x4)) = [1] + [-1]x4 + x3
POL(746_0_test_LE(x1)) = [1]
POL(751_0_test_Return) = [1]
POL(Cond_746_0_test_LE(x1, x2)) = [1]
POL(90_0_MAIN_GE(x1, x2)) = [-1] + x1
POL(COND_90_0_MAIN_GE(x1, x2, x3)) = [-1] + x2
POL(<(x1, x2)) = [-1]
POL(100) = [100]
POL(97_1_MAIN_INVOKEMETHOD(x1, x2, x3)) = [-1]x1 + x2
POL(COND_97_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4)) = [-1] + x3
POL(1) = [1]
POL(COND_90_0_MAIN_GE1(x1, x2, x3)) = [-1] + x2
POL(&&(x1, x2)) = [-1]
POL(99) = [99]
POL(-(x1, x2)) = x1 + [-1]x2
COND_90_0_MAIN_GE1(TRUE, x0[5], x1[5]) → 90_0_MAIN_GE(-(x0[5], 1), -(x0[5], 1))
90_0_MAIN_GE(x0[4], x1[4]) → COND_90_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])
90_0_MAIN_GE(x0[0], x1[0]) → COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])
COND_90_0_MAIN_GE(TRUE, x0[1], x1[1]) → 97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1[1]), x0[1], x1[1])
97_1_MAIN_INVOKEMETHOD(751_0_test_Return, x0[2], x1[2]) → COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])
COND_97_1_MAIN_INVOKEMETHOD(TRUE, 751_0_test_Return, x0[3], x1[3]) → 90_0_MAIN_GE(x0[3], +(x1[3], 1))
90_0_MAIN_GE(x0[4], x1[4]) → COND_90_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])
97_0_test_Load(x0)1 ↔ 356_0_test_LE(x0, x0, x0)1
356_0_test_LE(x0, 0, 0)1 ↔ 389_0_test_LE(x0, x0, x0)1
Cond_356_0_test_LE(TRUE, x0, x1, x1)1 ↔ 356_0_test_LE(x0, +(x1, -1), +(x1, -1))1
356_0_test_LE(x0, x1, x1)1 ↔ Cond_356_0_test_LE(>(x1, 0), x0, x1, x1)1
389_0_test_LE(x0, 0, 0)1 ↔ 416_0_test_LE(x0, x0, x0)1
Cond_389_0_test_LE(TRUE, x0, x1, x1)1 ↔ 389_0_test_LE(x0, +(x1, -1), +(x1, -1))1
389_0_test_LE(x0, x1, x1)1 ↔ Cond_389_0_test_LE(>(x1, 0), x0, x1, x1)1
416_0_test_LE(x0, 0, 0)1 ↔ 456_0_test_LE(x0, x0, x0)1
Cond_416_0_test_LE(TRUE, x0, x1, x1)1 ↔ 416_0_test_LE(x0, +(x1, -1), +(x1, -1))1
416_0_test_LE(x0, x1, x1)1 ↔ Cond_416_0_test_LE(>(x1, 0), x0, x1, x1)1
456_0_test_LE(x0, 0, 0)1 ↔ 496_0_test_LE(x0, x0, x0)1
Cond_456_0_test_LE(TRUE, x0, x1, x1)1 ↔ 456_0_test_LE(x0, +(x1, -1), +(x1, -1))1
456_0_test_LE(x0, x1, x1)1 ↔ Cond_456_0_test_LE(>(x1, 0), x0, x1, x1)1
496_0_test_LE(x0, 0, 0)1 ↔ 528_0_test_LE(x0, x0, x0)1
Cond_496_0_test_LE(TRUE, x0, x1, x1)1 ↔ 496_0_test_LE(x0, +(x1, -1), +(x1, -1))1
496_0_test_LE(x0, x1, x1)1 ↔ Cond_496_0_test_LE(>(x1, 0), x0, x1, x1)1
528_0_test_LE(x0, 0, 0)1 ↔ 564_0_test_LE(x0, x0, x0)1
Cond_528_0_test_LE(TRUE, x0, x1, x1)1 ↔ 528_0_test_LE(x0, +(x1, -1), +(x1, -1))1
528_0_test_LE(x0, x1, x1)1 ↔ Cond_528_0_test_LE(>(x1, 0), x0, x1, x1)1
564_0_test_LE(x0, 0, 0)1 ↔ 602_0_test_LE(x0, x0, x0)1
Cond_564_0_test_LE(TRUE, x0, x1, x1)1 ↔ 564_0_test_LE(x0, +(x1, -1), +(x1, -1))1
564_0_test_LE(x0, x1, x1)1 ↔ Cond_564_0_test_LE(>(x1, 0), x0, x1, x1)1
602_0_test_LE(x0, 0, 0)1 ↔ 641_0_test_LE(x0, x0, x0)1
Cond_602_0_test_LE(TRUE, x0, x1, x1)1 ↔ 602_0_test_LE(x0, +(x1, -1), +(x1, -1))1
602_0_test_LE(x0, x1, x1)1 ↔ Cond_602_0_test_LE(>(x1, 0), x0, x1, x1)1
641_0_test_LE(x0, 0, 0)1 ↔ 680_0_test_LE(x0, x0, x0)1
Cond_641_0_test_LE(TRUE, x0, x1, x1)1 ↔ 641_0_test_LE(x0, +(x1, -1), +(x1, -1))1
641_0_test_LE(x0, x1, x1)1 ↔ Cond_641_0_test_LE(>(x1, 0), x0, x1, x1)1
680_0_test_LE(x0, 0, 0)1 ↔ 715_0_test_LE(x0, x0, x0)1
Cond_680_0_test_LE(TRUE, x0, x1, x1)1 ↔ 680_0_test_LE(x0, +(x1, -1), +(x1, -1))1
680_0_test_LE(x0, x1, x1)1 ↔ Cond_680_0_test_LE(>(x1, 0), x0, x1, x1)1
715_0_test_LE(x0, 0, 0)1 ↔ 746_0_test_LE(x0)1
Cond_715_0_test_LE(TRUE, x0, x1, x1)1 ↔ 715_0_test_LE(x0, +(x1, -1), +(x1, -1))1
715_0_test_LE(x0, x1, x1)1 ↔ Cond_715_0_test_LE(>(x1, 0), x0, x1, x1)1
746_0_test_LE(0)1 ↔ 751_0_test_Return1
746_0_test_LE(x0)1 ↔ Cond_746_0_test_LE(>(x0, 0), x0)1
Cond_746_0_test_LE(TRUE, x0)1 ↔ 746_0_test_LE(+(x0, -1))1
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
(3) -> (0), if (x0[3] →* x0[0]∧x1[3] + 1 →* x1[0])
(0) -> (1), if (x1[0] < 100 ∧x0[0] →* x0[1]∧x1[0] →* x1[1])
(1) -> (2), if (97_0_test_Load(x1[1]) →* 751_0_test_Return∧x0[1] →* x0[2]∧x1[1] →* x1[2])
(2) -> (3), if (x1[2] > 0 ∧x0[2] →* x0[3]∧x1[2] →* x1[3])
(3) -> (4), if (x0[3] →* x0[4]∧x1[3] + 1 →* x1[4])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(3) -> (0), if (x0[3] →* x0[0]∧x1[3] + 1 →* x1[0])
(0) -> (1), if (x1[0] < 100 ∧x0[0] →* x0[1]∧x1[0] →* x1[1])
(1) -> (2), if (97_0_test_Load(x1[1]) →* 751_0_test_Return∧x0[1] →* x0[2]∧x1[1] →* x1[2])
(2) -> (3), if (x1[2] > 0 ∧x0[2] →* x0[3]∧x1[2] →* x1[3])
(1) (COND_97_1_MAIN_INVOKEMETHOD(TRUE, 751_0_test_Return, x0[3], x1[3])≥NonInfC∧COND_97_1_MAIN_INVOKEMETHOD(TRUE, 751_0_test_Return, x0[3], x1[3])≥90_0_MAIN_GE(x0[3], +(x1[3], 1))∧(UIncreasing(90_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥))
(2) ((UIncreasing(90_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_35] = 0∧[1 + (-1)bso_36] ≥ 0)
(3) ((UIncreasing(90_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_35] = 0∧[1 + (-1)bso_36] ≥ 0)
(4) ((UIncreasing(90_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_35] = 0∧[1 + (-1)bso_36] ≥ 0)
(5) ((UIncreasing(90_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_35] = 0∧0 = 0∧[1 + (-1)bso_36] ≥ 0)
(6) (>(x1[2], 0)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3] ⇒ 97_1_MAIN_INVOKEMETHOD(751_0_test_Return, x0[2], x1[2])≥NonInfC∧97_1_MAIN_INVOKEMETHOD(751_0_test_Return, x0[2], x1[2])≥COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])∧(UIncreasing(COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])), ≥))
(7) (>(x1[2], 0)=TRUE ⇒ 97_1_MAIN_INVOKEMETHOD(751_0_test_Return, x0[2], x1[2])≥NonInfC∧97_1_MAIN_INVOKEMETHOD(751_0_test_Return, x0[2], x1[2])≥COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])∧(UIncreasing(COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])), ≥))
(8) (x1[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])), ≥)∧[(-1)bni_37 + (-1)Bound*bni_37] + [(-1)bni_37]x1[2] ≥ 0∧[(-1)bso_38] ≥ 0)
(9) (x1[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])), ≥)∧[(-1)bni_37 + (-1)Bound*bni_37] + [(-1)bni_37]x1[2] ≥ 0∧[(-1)bso_38] ≥ 0)
(10) (x1[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])), ≥)∧[(-1)bni_37 + (-1)Bound*bni_37] + [(-1)bni_37]x1[2] ≥ 0∧[(-1)bso_38] ≥ 0)
(11) (x1[2] ≥ 0 ⇒ (UIncreasing(COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])), ≥)∧[(-2)bni_37 + (-1)Bound*bni_37] + [(-1)bni_37]x1[2] ≥ 0∧[(-1)bso_38] ≥ 0)
(12) (COND_90_0_MAIN_GE(TRUE, x0[1], x1[1])≥NonInfC∧COND_90_0_MAIN_GE(TRUE, x0[1], x1[1])≥97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1[1]), x0[1], x1[1])∧(UIncreasing(97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1[1]), x0[1], x1[1])), ≥))
(13) ((UIncreasing(97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_39] = 0∧[(-1)bso_40] ≥ 0)
(14) ((UIncreasing(97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_39] = 0∧[(-1)bso_40] ≥ 0)
(15) ((UIncreasing(97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_39] = 0∧[(-1)bso_40] ≥ 0)
(16) ((UIncreasing(97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_39] = 0∧0 = 0∧[(-1)bso_40] ≥ 0)
(17) (<(x1[0], 100)=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1] ⇒ 90_0_MAIN_GE(x0[0], x1[0])≥NonInfC∧90_0_MAIN_GE(x0[0], x1[0])≥COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])∧(UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥))
(18) (<(x1[0], 100)=TRUE ⇒ 90_0_MAIN_GE(x0[0], x1[0])≥NonInfC∧90_0_MAIN_GE(x0[0], x1[0])≥COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])∧(UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥))
(19) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [(-1)bni_41]x1[0] ≥ 0∧[(-1)bso_42] ≥ 0)
(20) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [(-1)bni_41]x1[0] ≥ 0∧[(-1)bso_42] ≥ 0)
(21) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [(-1)bni_41]x1[0] ≥ 0∧[(-1)bso_42] ≥ 0)
(22) ([99] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [(-1)bni_41]x1[0] ≥ 0∧[(-1)bso_42] ≥ 0)
(23) ([99] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [bni_41]x1[0] ≥ 0∧[(-1)bso_42] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(97_0_test_Load(x1)) = [-1] + x1
POL(356_0_test_LE(x1, x2, x3)) = [1] + [-1]x3 + x2
POL(Cond_356_0_test_LE(x1, x2, x3, x4)) = [-1] + [-1]x3 + x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(389_0_test_LE(x1, x2, x3)) = [1] + [-1]x3 + [-1]x2 + [-1]x1
POL(Cond_389_0_test_LE(x1, x2, x3, x4)) = x4 + [-1]x3 + x2
POL(416_0_test_LE(x1, x2, x3)) = [2] + [2]x3 + [-1]x2
POL(Cond_416_0_test_LE(x1, x2, x3, x4)) = [2]x3 + x2
POL(456_0_test_LE(x1, x2, x3)) = [-1]x2
POL(Cond_456_0_test_LE(x1, x2, x3, x4)) = [2]x4 + x2
POL(496_0_test_LE(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2 + [-1]x1
POL(Cond_496_0_test_LE(x1, x2, x3, x4)) = [-1] + [2]x4 + [-1]x3 + x2
POL(528_0_test_LE(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2 + [-1]x1
POL(Cond_528_0_test_LE(x1, x2, x3, x4)) = [-1] + [2]x4 + [-1]x3 + x2
POL(564_0_test_LE(x1, x2, x3)) = [1] + [2]x3 + x2
POL(Cond_564_0_test_LE(x1, x2, x3, x4)) = [2] + [2]x3 + x2
POL(602_0_test_LE(x1, x2, x3)) = [2] + [-1]x3 + [-1]x1
POL(Cond_602_0_test_LE(x1, x2, x3, x4)) = [-1] + [-1]x4 + [-1]x3 + x2
POL(641_0_test_LE(x1, x2, x3)) = [-1]x3 + [-1]x2
POL(Cond_641_0_test_LE(x1, x2, x3, x4)) = [-1] + [-1]x3 + x2
POL(680_0_test_LE(x1, x2, x3)) = [-1]x3 + [-1]x2 + [2]x1
POL(Cond_680_0_test_LE(x1, x2, x3, x4)) = [-1] + [2]x4 + [-1]x3 + x2
POL(715_0_test_LE(x1, x2, x3)) = [-1]x3 + [-1]x2 + x1
POL(Cond_715_0_test_LE(x1, x2, x3, x4)) = [-1] + [2]x4 + [-1]x3 + x2
POL(746_0_test_LE(x1)) = 0
POL(751_0_test_Return) = [-1]
POL(Cond_746_0_test_LE(x1, x2)) = [2] + x2
POL(COND_97_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4)) = [-1] + [-1]x4
POL(90_0_MAIN_GE(x1, x2)) = [-1] + [-1]x2
POL(1) = [1]
POL(97_1_MAIN_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x3
POL(COND_90_0_MAIN_GE(x1, x2, x3)) = [-1] + [-1]x3
POL(<(x1, x2)) = [-1]
POL(100) = [100]
COND_97_1_MAIN_INVOKEMETHOD(TRUE, 751_0_test_Return, x0[3], x1[3]) → 90_0_MAIN_GE(x0[3], +(x1[3], 1))
90_0_MAIN_GE(x0[0], x1[0]) → COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])
97_1_MAIN_INVOKEMETHOD(751_0_test_Return, x0[2], x1[2]) → COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])
COND_90_0_MAIN_GE(TRUE, x0[1], x1[1]) → 97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1[1]), x0[1], x1[1])
90_0_MAIN_GE(x0[0], x1[0]) → COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])
680_0_test_LE(x0, x0, x0)1 → 641_0_test_LE(x0, 0, 0)1
746_0_test_LE(0)1 → 751_0_test_Return1
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x1[0] < 100 ∧x0[0] →* x0[1]∧x1[0] →* x1[1])
(1) -> (2), if (97_0_test_Load(x1[1]) →* 751_0_test_Return∧x0[1] →* x0[2]∧x1[1] →* x1[2])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(1) -> (2), if (97_0_test_Load(x1[1]) →* 751_0_test_Return∧x0[1] →* x0[2]∧x1[1] →* x1[2])
(2) -> (3), if (x1[2] > 0 ∧x0[2] →* x0[3]∧x1[2] →* x1[3])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(3) -> (0), if (x0[3] →* x0[0]∧x1[3] + 1 →* x1[0])
(5) -> (0), if (x0[5] - 1 →* x0[0]∧x0[5] - 1 →* x1[0])
(0) -> (1), if (x1[0] < 100 ∧x0[0] →* x0[1]∧x1[0] →* x1[1])
(1) -> (2), if (97_0_test_Load(x1[1]) →* 751_0_test_Return∧x0[1] →* x0[2]∧x1[1] →* x1[2])
(2) -> (3), if (x1[2] > 0 ∧x0[2] →* x0[3]∧x1[2] →* x1[3])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(3) -> (0), if (x0[3] →* x0[0]∧x1[3] + 1 →* x1[0])
(0) -> (1), if (x1[0] < 100 ∧x0[0] →* x0[1]∧x1[0] →* x1[1])
(1) -> (2), if (97_0_test_Load(x1[1]) →* 751_0_test_Return∧x0[1] →* x0[2]∧x1[1] →* x1[2])
(2) -> (3), if (x1[2] > 0 ∧x0[2] →* x0[3]∧x1[2] →* x1[3])
(1) (COND_97_1_MAIN_INVOKEMETHOD(TRUE, 751_0_test_Return, x0[3], x1[3])≥NonInfC∧COND_97_1_MAIN_INVOKEMETHOD(TRUE, 751_0_test_Return, x0[3], x1[3])≥90_0_MAIN_GE(x0[3], +(x1[3], 1))∧(UIncreasing(90_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥))
(2) ((UIncreasing(90_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_36] = 0∧[1 + (-1)bso_37] ≥ 0)
(3) ((UIncreasing(90_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_36] = 0∧[1 + (-1)bso_37] ≥ 0)
(4) ((UIncreasing(90_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_36] = 0∧[1 + (-1)bso_37] ≥ 0)
(5) ((UIncreasing(90_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_36] = 0∧0 = 0∧[1 + (-1)bso_37] ≥ 0)
(6) (>(x1[2], 0)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3] ⇒ 97_1_MAIN_INVOKEMETHOD(751_0_test_Return, x0[2], x1[2])≥NonInfC∧97_1_MAIN_INVOKEMETHOD(751_0_test_Return, x0[2], x1[2])≥COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])∧(UIncreasing(COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])), ≥))
(7) (>(x1[2], 0)=TRUE ⇒ 97_1_MAIN_INVOKEMETHOD(751_0_test_Return, x0[2], x1[2])≥NonInfC∧97_1_MAIN_INVOKEMETHOD(751_0_test_Return, x0[2], x1[2])≥COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])∧(UIncreasing(COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])), ≥))
(8) (x1[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])), ≥)∧[(-1)bni_38 + (-1)Bound*bni_38] + [(-1)bni_38]x1[2] ≥ 0∧[(-1)bso_39] ≥ 0)
(9) (x1[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])), ≥)∧[(-1)bni_38 + (-1)Bound*bni_38] + [(-1)bni_38]x1[2] ≥ 0∧[(-1)bso_39] ≥ 0)
(10) (x1[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])), ≥)∧[(-1)bni_38 + (-1)Bound*bni_38] + [(-1)bni_38]x1[2] ≥ 0∧[(-1)bso_39] ≥ 0)
(11) (x1[2] ≥ 0 ⇒ (UIncreasing(COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])), ≥)∧[(-2)bni_38 + (-1)Bound*bni_38] + [(-1)bni_38]x1[2] ≥ 0∧[(-1)bso_39] ≥ 0)
(12) (COND_90_0_MAIN_GE(TRUE, x0[1], x1[1])≥NonInfC∧COND_90_0_MAIN_GE(TRUE, x0[1], x1[1])≥97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1[1]), x0[1], x1[1])∧(UIncreasing(97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1[1]), x0[1], x1[1])), ≥))
(13) ((UIncreasing(97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_40] = 0∧[(-1)bso_41] ≥ 0)
(14) ((UIncreasing(97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_40] = 0∧[(-1)bso_41] ≥ 0)
(15) ((UIncreasing(97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_40] = 0∧[(-1)bso_41] ≥ 0)
(16) ((UIncreasing(97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_40] = 0∧0 = 0∧[(-1)bso_41] ≥ 0)
(17) (<(x1[0], 100)=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1] ⇒ 90_0_MAIN_GE(x0[0], x1[0])≥NonInfC∧90_0_MAIN_GE(x0[0], x1[0])≥COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])∧(UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥))
(18) (<(x1[0], 100)=TRUE ⇒ 90_0_MAIN_GE(x0[0], x1[0])≥NonInfC∧90_0_MAIN_GE(x0[0], x1[0])≥COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])∧(UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥))
(19) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [(-1)bni_42]x1[0] ≥ 0∧[(-1)bso_43] ≥ 0)
(20) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [(-1)bni_42]x1[0] ≥ 0∧[(-1)bso_43] ≥ 0)
(21) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [(-1)bni_42]x1[0] ≥ 0∧[(-1)bso_43] ≥ 0)
(22) ([99] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [(-1)bni_42]x1[0] ≥ 0∧[(-1)bso_43] ≥ 0)
(23) ([99] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]x1[0] ≥ 0∧[(-1)bso_43] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(97_0_test_Load(x1)) = [-1] + [-1]x1
POL(356_0_test_LE(x1, x2, x3)) = [-1] + [-1]x2 + [-1]x1
POL(Cond_356_0_test_LE(x1, x2, x3, x4)) = [-1] + [-1]x4 + [-1]x2
POL(>(x1, x2)) = 0
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(389_0_test_LE(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2 + [-1]x1
POL(Cond_389_0_test_LE(x1, x2, x3, x4)) = [-1] + [2]x4 + [-1]x3 + [-1]x2
POL(416_0_test_LE(x1, x2, x3)) = [-1]x3 + [-1]x2 + x1
POL(Cond_416_0_test_LE(x1, x2, x3, x4)) = [-1] + [-1]x4 + [-1]x3 + [-1]x2
POL(456_0_test_LE(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2 + [-1]x1
POL(Cond_456_0_test_LE(x1, x2, x3, x4)) = [-1] + [-1]x4 + [-1]x3 + [-1]x2
POL(496_0_test_LE(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2 + [-1]x1
POL(Cond_496_0_test_LE(x1, x2, x3, x4)) = [-1] + [2]x4 + [-1]x3 + [-1]x2
POL(528_0_test_LE(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2 + x1
POL(Cond_528_0_test_LE(x1, x2, x3, x4)) = [-1] + [2]x4 + [-1]x3 + [-1]x2
POL(564_0_test_LE(x1, x2, x3)) = [2] + [-1]x3 + x2 + [-1]x1
POL(Cond_564_0_test_LE(x1, x2, x3, x4)) = [-1] + [-1]x4 + [-1]x3 + [-1]x2
POL(602_0_test_LE(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2 + [-1]x1
POL(Cond_602_0_test_LE(x1, x2, x3, x4)) = [-1] + [2]x4 + [-1]x3 + [-1]x2
POL(641_0_test_LE(x1, x2, x3)) = [1] + [-1]x3 + [-1]x2 + [-1]x1
POL(Cond_641_0_test_LE(x1, x2, x3, x4)) = [1] + [-1]x4 + [-1]x3 + [-1]x2
POL(680_0_test_LE(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2 + [2]x1
POL(Cond_680_0_test_LE(x1, x2, x3, x4)) = [-1] + [2]x4 + [-1]x3 + [-1]x2
POL(715_0_test_LE(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2 + [-1]x1
POL(Cond_715_0_test_LE(x1, x2, x3, x4)) = [-1] + [2]x4 + [-1]x3 + [-1]x2
POL(746_0_test_LE(x1)) = [-1]
POL(751_0_test_Return) = [2]
POL(Cond_746_0_test_LE(x1, x2)) = [-1] + [-1]x2
POL(COND_97_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4)) = [-1] + [-1]x4
POL(90_0_MAIN_GE(x1, x2)) = [-1] + [-1]x2
POL(1) = [1]
POL(97_1_MAIN_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x3
POL(COND_90_0_MAIN_GE(x1, x2, x3)) = [-1] + [-1]x3
POL(<(x1, x2)) = [2]
POL(100) = [100]
COND_97_1_MAIN_INVOKEMETHOD(TRUE, 751_0_test_Return, x0[3], x1[3]) → 90_0_MAIN_GE(x0[3], +(x1[3], 1))
90_0_MAIN_GE(x0[0], x1[0]) → COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])
97_1_MAIN_INVOKEMETHOD(751_0_test_Return, x0[2], x1[2]) → COND_97_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 751_0_test_Return, x0[2], x1[2])
COND_90_0_MAIN_GE(TRUE, x0[1], x1[1]) → 97_1_MAIN_INVOKEMETHOD(97_0_test_Load(x1[1]), x0[1], x1[1])
90_0_MAIN_GE(x0[0], x1[0]) → COND_90_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])
416_0_test_LE(x0, x0, x0)1 → 389_0_test_LE(x0, 0, 0)1
456_0_test_LE(x0, +(x1, -1), +(x1, -1))1 → Cond_456_0_test_LE(TRUE, x0, x1, x1)1
456_0_test_LE(x0, x1, x1)1 ↔ Cond_456_0_test_LE(>(x1, 0), x0, x1, x1)1
528_0_test_LE(x0, x0, x0)1 → 496_0_test_LE(x0, 0, 0)1
641_0_test_LE(x0, +(x1, -1), +(x1, -1))1 → Cond_641_0_test_LE(TRUE, x0, x1, x1)1
641_0_test_LE(x0, x1, x1)1 ↔ Cond_641_0_test_LE(>(x1, 0), x0, x1, x1)1
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x1[0] < 100 ∧x0[0] →* x0[1]∧x1[0] →* x1[1])
(1) -> (2), if (97_0_test_Load(x1[1]) →* 751_0_test_Return∧x0[1] →* x0[2]∧x1[1] →* x1[2])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(1) -> (2), if (97_0_test_Load(x1[1]) →* 751_0_test_Return∧x0[1] →* x0[2]∧x1[1] →* x1[2])
(2) -> (3), if (x1[2] > 0 ∧x0[2] →* x0[3]∧x1[2] →* x1[3])